MathlibAnnex/Topology/ClosureSpace/LinkedSet.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6module78public import MathlibAnnex.Topology.ClosureSpace.Components9public import Mathlib.Order.Minimal1011/-!12# Sets of pairwise linked points1314These are the R-sets of Definition 6.11. The empty set is permitted. Maximality15is the existing order-theoretic `Maximal` predicate on sets ordered by inclusion,16not a new structure postulating any geometric classification.17-/1819@[expose] public section2021set_option autoImplicit false2223universe u v2425namespace ClosureSpace2627variable {α : Type u} {β : Type v}2829/-- Every two points of the set are linked in the ambient closure space. -/30def IsLinkedSet (c : ClosureSpace α) (S : Set α) : Prop :=31  ∀ x ∈ S, ∀ y ∈ S, c.Linked x y3233/-- The empty set is an R-set, with no nonemptiness convention added. -/34theorem isLinkedSet_empty (c : ClosureSpace α) : c.IsLinkedSet ∅ := by35  intro x hx36  exact hx.elim3738/-- Reflexivity of `Linked` makes every singleton an R-set. -/39theorem isLinkedSet_singleton (c : ClosureSpace α) (x : α) : c.IsLinkedSet {x} := by40  rintro y rfl z rfl41  exact c.linked_refl _4243/-- Taking a subset preserves pairwise linkedness. -/44theorem IsLinkedSet.mono {c : ClosureSpace α} {S T : Set α}45    (hT : c.IsLinkedSet T) (hST : S ⊆ T) : c.IsLinkedSet S :=46  fun x hx y hy => hT x (hST hx) y (hST hy)4748/-- The pairwise condition agrees with the existing two-point relation. -/49theorem isLinkedSet_pair_iff (c : ClosureSpace α) (x y : α) :50    c.IsLinkedSet {x, y} ↔ c.Linked x y := by51  constructor52  · intro h53    exact h x (by simp) y (by simp)54  · intro h a ha b hb55    rcases (show a = x ∨ a = y by simpa only [Set.mem_insert_iff, Set.mem_singleton_iff] using ha)56      with hax | hay <;>57      rcases (show b = x ∨ b = y by simpa only [Set.mem_insert_iff, Set.mem_singleton_iff] using hb)58        with hbx | hby59    · subst a; subst b; exact c.linked_refl x60    · subst a; subst b; exact h61    · subst a; subst b; exact c.linked_symm h62    · subst a; subst b; exact c.linked_refl y6364/-- To insert one point, it suffices and is necessary to link it to every old point. -/65theorem isLinkedSet_insert_iff (c : ClosureSpace α) (x : α) (S : Set α) :66    c.IsLinkedSet (insert x S) ↔ c.IsLinkedSet S ∧ ∀ y ∈ S, c.Linked x y := by67  constructor68  · intro h69    exact ⟨h.mono (Set.subset_insert x S), fun y hy => h x (by simp) y (Or.inr hy)⟩70  · rintro ⟨hS, hx⟩ a ha b hb71    rcases Set.mem_insert_iff.mp ha with hax | ha <;>72      rcases Set.mem_insert_iff.mp hb with hbx | hb73    · subst a; subst b; exact c.linked_refl x74    · subst a; exact hx b hb75    · subst b; exact c.linked_symm (hx a ha)76    · exact hS a ha b hb7778/-- A nonempty R-set lies in the component of any of its points. -/79theorem IsLinkedSet.subset_component {c : ClosureSpace α} {S : Set α}80    (hS : c.IsLinkedSet S) {x : α} (hx : x ∈ S) : S ⊆ c.component x :=81  fun y hy => c.related_of_linked (hS x hx y hy)8283/-- Finite continuity and injectivity are enough for images of R-sets. -/84theorem FinitelyContinuous.isLinkedSet_image {c : ClosureSpace α} {d : ClosureSpace β}85    {f : α → β} (hf : c.FinitelyContinuous d f) (hinj : Function.Injective f)86    {S : Set α} (hS : c.IsLinkedSet S) : d.IsLinkedSet (f '' S) := by87  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩88  exact hf.linked hinj (hS x hx y hy)8990end ClosureSpace