Mathlib.Topology.Sets.Opens

TopologicalSpace.Opens structure

Full source

/-- The type of open subsets of a topological space. -/
structure Opens where
  /-- The underlying set of a bundled `TopologicalSpace.Opens` object. -/
  carrier : Set α
  /-- The `TopologicalSpace.Opens.carrier _` is an open set. -/
  is_open' : IsOpen carrier

Open subsets of a topological space

Informal description

The structure representing the type of open subsets of a topological space $\alpha$. An element of this type is a subset of $\alpha$ that is open in the given topology.

TopologicalSpace.Opens.instSetLike instance

: SetLike (Opens α) α

Full source

instance : SetLike (Opens α) α where
  coe := Opens.carrier
  coe_injective' := fun ⟨_, _⟩ ⟨_, _⟩ _ => by congr

Open Sets as Sets in a Topological Space

Informal description

The type of open subsets of a topological space $\alpha$ is equipped with a `SetLike` structure, allowing its elements to be treated as sets of elements of $\alpha$.

TopologicalSpace.Opens.instCanLiftSetCoeIsOpen instance

: CanLift (Set α) (Opens α) (↑) IsOpen

Full source

instance : CanLift (Set α) (Opens α) (↑) IsOpen :=
  ⟨fun s h => ⟨⟨s, h⟩, rfl⟩⟩

Lifting Condition from Subsets to Open Subsets

Informal description

For any topological space $\alpha$, there is a canonical way to lift a subset $U$ of $\alpha$ to an open subset of $\alpha$ (an element of `Opens α`) if and only if $U$ is open in $\alpha$.

TopologicalSpace.Opens.instSecondCountableOpens instance

[SecondCountableTopology α] (U : Opens α) : SecondCountableTopology U

Full source

instance instSecondCountableOpens [SecondCountableTopology α] (U : Opens α) :
    SecondCountableTopology U := inferInstanceAs (SecondCountableTopology U.1)

Second-Countability of Open Subsets in Second-Countable Spaces

Informal description

For any topological space $\alpha$ with a second-countable topology and any open subset $U$ of $\alpha$, the subspace topology on $U$ is also second-countable.

TopologicalSpace.Opens.forall theorem

{p : Opens α → Prop} : (∀ U, p U) ↔ ∀ (U : Set α) (hU : IsOpen U), p ⟨U, hU⟩

Full source

theorem «forall» {p : Opens α → Prop} : (∀ U, p U) ↔ ∀ (U : Set α) (hU : IsOpen U), p ⟨U, hU⟩ :=
  ⟨fun h _ _ => h _, fun h _ => h _ _⟩

Universal Quantification over Open Subsets vs Open Sets

Informal description

For any predicate $p$ on open subsets of a topological space $\alpha$, the universal quantification over all open subsets $U$ of $\alpha$ (i.e., $\forall U \in \text{Opens}(\alpha), p(U)$) is equivalent to the universal quantification over all subsets $U$ of $\alpha$ that are open (i.e., $\forall U \subseteq \alpha, \text{IsOpen}(U) \rightarrow p(\langle U, \text{IsOpen}(U) \rangle)$).

TopologicalSpace.Opens.carrier_eq_coe theorem

(U : Opens α) : U.1 = ↑U

Full source

@[simp] theorem carrier_eq_coe (U : Opens α) : U.1 = ↑U := rfl

Underlying Set of Open Subset Equals its Coercion

Informal description

For any open subset $U$ of a topological space $\alpha$, the underlying set $U.1$ is equal to the coercion of $U$ to a set (denoted by $\uparrow U$).

TopologicalSpace.Opens.coe_mk theorem

{U : Set α} {hU : IsOpen U} : ↑(⟨U, hU⟩ : Opens α) = U

Full source

/-- the coercion `Opens α → Set α` applied to a pair is the same as taking the first component -/
@[simp]
theorem coe_mk {U : Set α} {hU : IsOpen U} : ↑(⟨U, hU⟩ : Opens α) = U :=
  rfl

Coercion of Bundled Open Set to Set Equals Original Set

Informal description

For any open set $U$ in a topological space $\alpha$ with proof $h_U$ that $U$ is open, the coercion from the bundled open set $\langle U, h_U \rangle$ to a plain set equals $U$ itself, i.e., $\langle U, h_U \rangle = U$.

TopologicalSpace.Opens.mem_mk theorem

{x : α} {U : Set α} {h : IsOpen U} : x ∈ mk U h ↔ x ∈ U

Full source

@[simp]
theorem mem_mk {x : α} {U : Set α} {h : IsOpen U} : x ∈ mk U hx ∈ mk U h ↔ x ∈ U := Iff.rfl

Membership in Bundled Open Set Equals Membership in Underlying Set

Informal description

For any point $x$ in a topological space $\alpha$, any subset $U$ of $\alpha$, and any proof $h$ that $U$ is open, the point $x$ belongs to the bundled open set $\langle U, h \rangle$ if and only if $x$ belongs to $U$.

TopologicalSpace.Opens.nonempty_coeSort theorem

{U : Opens α} : Nonempty U ↔ (U : Set α).Nonempty

Full source

protected theorem nonempty_coeSort {U : Opens α} : NonemptyNonempty U ↔ (U : Set α).Nonempty :=
  Set.nonempty_coe_sort

Nonempty Open Subset Characterization via Type and Set

Informal description

For any open subset $U$ of a topological space $\alpha$, the type $U$ is nonempty if and only if the underlying set $U$ is nonempty.

TopologicalSpace.Opens.nonempty_coe theorem

{U : Opens α} : (U : Set α).Nonempty ↔ ∃ x, x ∈ U

Full source

protected theorem nonempty_coe {U : Opens α} : (U : Set α).Nonempty ↔ ∃ x, x ∈ U :=
  Iff.rfl

Nonempty Open Subset Characterization

Informal description

For any open subset $U$ of a topological space $\alpha$, the set $U$ is nonempty if and only if there exists an element $x \in \alpha$ such that $x \in U$.

TopologicalSpace.Opens.ext theorem

{U V : Opens α} (h : (U : Set α) = V) : U = V

Full source

@[ext] -- TODO: replace with `∀ x, x ∈ U ↔ x ∈ V`?
theorem ext {U V : Opens α} (h : (U : Set α) = V) : U = V :=
  SetLike.coe_injective h

Equality of Open Subsets via Underlying Set Equality

Informal description

For any two open subsets $U$ and $V$ of a topological space $\alpha$, if their underlying sets are equal (i.e., $U = V$ as sets), then $U$ and $V$ are equal as elements of the type `TopologicalSpace.Opens α`.

TopologicalSpace.Opens.coe_inj theorem

{U V : Opens α} : (U : Set α) = V ↔ U = V

Full source

theorem coe_inj {U V : Opens α} : (U : Set α) = V ↔ U = V :=
  SetLike.ext'_iff.symm

Equality of Open Subsets via Underlying Set Equality

Informal description

For any two open subsets $U$ and $V$ of a topological space $\alpha$, the underlying sets of $U$ and $V$ are equal if and only if $U$ and $V$ are equal as elements of the type of open subsets.

TopologicalSpace.Opens.inclusion abbrev

{U V : Opens α} (h : U ≤ V) : U → V

Full source

/-- A version of `Set.inclusion` not requiring definitional abuse -/
abbrev inclusion {U V : Opens α} (h : U ≤ V) : U → V := Set.inclusion h

Inclusion Map Between Open Subsets

Informal description

For any two open subsets $U$ and $V$ of a topological space $\alpha$ such that $U \subseteq V$, there exists an inclusion map from $U$ to $V$ that sends each element of $U$ to itself as an element of $V$.

TopologicalSpace.Opens.isOpen theorem

(U : Opens α) : IsOpen (U : Set α)

Full source

protected theorem isOpen (U : Opens α) : IsOpen (U : Set α) :=
  U.is_open'

Openness of Underlying Set in `Opens α`

Informal description

For any open set $U$ in a topological space $\alpha$, the underlying subset of $\alpha$ corresponding to $U$ is open.

TopologicalSpace.Opens.mk_coe theorem

(U : Opens α) : mk (↑U) U.isOpen = U

Full source

@[simp] theorem mk_coe (U : Opens α) : mk (↑U) U.isOpen = U := rfl

Construction of Open Set from Its Underlying Subset Yields Itself

Informal description

For any open set $U$ in a topological space $\alpha$, the construction of an open set from the underlying subset of $U$ and its openness property yields $U$ itself.

TopologicalSpace.Opens.Simps.coe definition

(U : Opens α) : Set α

Full source

/-- See Note [custom simps projection]. -/
def Simps.coe (U : Opens α) : Set α := U

Underlying subset of an open set

Informal description

The coercion function that maps an open set $U$ in a topological space $\alpha$ to its underlying subset of $\alpha$.

TopologicalSpace.Opens.interior definition

(s : Set α) : Opens α

Full source

/-- The interior of a set, as an element of `Opens`. -/
@[simps]
protected def interior (s : Set α) : Opens α :=
  ⟨interior s, isOpen_interior⟩

Interior of a subset as an open set

Informal description

The function that takes a subset $s$ of a topological space $\alpha$ and returns its interior as an open set in $\alpha$. The interior of $s$ is the largest open set contained in $s$.

TopologicalSpace.Opens.mem_interior theorem

{s : Set α} {x : α} : x ∈ Opens.interior s ↔ x ∈ _root_.interior s

Full source

@[simp]
theorem mem_interior {s : Set α} {x : α} : x ∈ Opens.interior sx ∈ Opens.interior s ↔ x ∈ _root_.interior s := .rfl

Equivalence of Membership in Interior as Open Set and Topological Interior

Informal description

For any subset $s$ of a topological space $\alpha$ and any point $x \in \alpha$, $x$ belongs to the interior of $s$ (as an open set) if and only if $x$ belongs to the topological interior of $s$.

TopologicalSpace.Opens.gc theorem

: GaloisConnection ((↑) : Opens α → Set α) Opens.interior

Full source

theorem gc : GaloisConnection ((↑) : Opens α → Set α) Opens.interior := fun U _ =>
  ⟨fun h => interior_maximal h U.isOpen, fun h => le_trans h interior_subset⟩

Galois Connection Between Open Sets and Interior Operator

Informal description

The pair of functions consisting of the coercion from open sets to sets and the interior operator forms a Galois connection. That is, for any open set $U$ and any subset $s$ of a topological space $\alpha$, we have $U \subseteq \text{interior}(s)$ if and only if $U \subseteq s$ (where $U$ is considered as a subset via the coercion).

TopologicalSpace.Opens.gi definition

: GaloisCoinsertion (↑) (@Opens.interior α _)

Full source

/-- The galois coinsertion between sets and opens. -/
def gi : GaloisCoinsertion (↑) (@Opens.interior α _) where
  choice s hs := ⟨s, interior_eq_iff_isOpen.mp <| le_antisymm interior_subset hs⟩
  gc := gc
  u_l_le _ := interior_subset
  choice_eq _s hs := le_antisymm hs interior_subset

Galois coinsertion between open sets and interior operator

Informal description

The pair of functions consisting of the coercion from open sets to sets and the interior operator forms a Galois coinsertion. That is, for any subset $s$ of a topological space $\alpha$, the interior of $s$ is the largest open set contained in $s$, and the coercion from open sets to sets is its left adjoint. Specifically: 1. For any subset $s$, the interior $\text{interior}(s)$ is an open set. 2. The coercion and interior form a Galois connection. 3. The interior of an open set $U$ is $U$ itself. 4. The choice function selects the largest open set contained in $s$ when $s$ contains its interior.

TopologicalSpace.Opens.instCompleteLattice instance

: CompleteLattice (Opens α)

Full source

instance : CompleteLattice (Opens α) :=
  CompleteLattice.copy (GaloisCoinsertion.liftCompleteLattice gi)
    -- le
    (fun U V => (U : Set α) ⊆ V) rfl
    -- top
    ⟨univ, isOpen_univ⟩ (ext interior_univ.symm)
    -- bot
    ⟨∅, isOpen_empty⟩ rfl
    -- sup
    (fun U V => ⟨↑U ∪ ↑V, U.2.union V.2⟩) rfl
    -- inf
    (fun U V => ⟨↑U ∩ ↑V, U.2.inter V.2⟩)
    (funext₂ fun U V => ext (U.2.inter V.2).interior_eq.symm)
    -- sSup
    (fun S => ⟨⋃ s ∈ S, ↑s, isOpen_biUnion fun s _ => s.2⟩)
    (funext fun _ => ext sSup_image.symm)
    -- sInf
    _ rfl

Complete Lattice Structure on Open Sets

Informal description

The collection of open subsets of a topological space $\alpha$ forms a complete lattice, where the order is given by inclusion, the meet is intersection, and the join is the interior of the union.

TopologicalSpace.Opens.mk_inf_mk theorem

 {U V : Set α} {hU : IsOpen U} {hV : IsOpen V} : (⟨U, hU⟩ ⊓ ⟨V, hV⟩ : Opens α) = ⟨U ⊓ V, IsOpen.inter hU hV⟩

Full source

@[simp]
theorem mk_inf_mk {U V : Set α} {hU : IsOpen U} {hV : IsOpen V} :
    (⟨U, hU⟩⟨U, hU⟩ ⊓ ⟨V, hV⟩ : Opens α) = ⟨U ⊓ V, IsOpen.inter hU hV⟩ :=
  rfl

Meet of Bundled Open Sets is Intersection

Informal description

For any two open subsets $U$ and $V$ of a topological space $\alpha$, the meet (infimum) of the bundled open sets $\langle U, hU \rangle$ and $\langle V, hV \rangle$ in the complete lattice of open sets is equal to the bundled open set $\langle U \cap V, \text{IsOpen.inter } hU \ hV \rangle$, where $hU$ and $hV$ are proofs that $U$ and $V$ are open, respectively.

TopologicalSpace.Opens.coe_inf theorem

(s t : Opens α) : (↑(s ⊓ t) : Set α) = ↑s ∩ ↑t

Full source

@[simp, norm_cast]
theorem coe_inf (s t : Opens α) : (↑(s ⊓ t) : Set α) = ↑s ∩ ↑t :=
  rfl

Infimum of Open Sets as Intersection

Informal description

For any two open sets $s$ and $t$ in a topological space $\alpha$, the underlying set of their infimum $s \sqcap t$ is equal to the intersection of the underlying sets of $s$ and $t$, i.e., $(s \sqcap t) = s \cap t$.

TopologicalSpace.Opens.mem_inf theorem

{s t : Opens α} {x : α} : x ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t

Full source

@[simp]
lemma mem_inf {s t : Opens α} {x : α} : x ∈ s ⊓ tx ∈ s ⊓ t ↔ x ∈ s ∧ x ∈ t := Iff.rfl

Membership in Intersection of Open Sets

Informal description

For any open sets $s$ and $t$ in a topological space $\alpha$ and any point $x \in \alpha$, $x$ belongs to the intersection $s \sqcap t$ if and only if $x$ belongs to both $s$ and $t$.

TopologicalSpace.Opens.coe_sup theorem

(s t : Opens α) : (↑(s ⊔ t) : Set α) = ↑s ∪ ↑t

Full source

@[simp, norm_cast]
theorem coe_sup (s t : Opens α) : (↑(s ⊔ t) : Set α) = ↑s ∪ ↑t :=
  rfl

Supremum of Open Sets as Union

Informal description

For any two open sets $s$ and $t$ in a topological space $\alpha$, the underlying set of their supremum $s \sqcup t$ is equal to the union of the underlying sets of $s$ and $t$, i.e., $(s \sqcup t) = s \cup t$.

TopologicalSpace.Opens.coe_bot theorem

: ((⊥ : Opens α) : Set α) = ∅

Full source

@[simp, norm_cast]
theorem coe_bot : ((⊥ : Opens α) : Set α) = ∅ :=
  rfl

Bottom Open Set is Empty Set

Informal description

The bottom element of the complete lattice of open subsets of a topological space $\alpha$ corresponds to the empty set, i.e., $\bot = \emptyset$.

TopologicalSpace.Opens.mem_bot theorem

{x : α} : x ∈ (⊥ : Opens α) ↔ False

Full source

@[simp]
lemma mem_bot {x : α} : x ∈ (⊥ : Opens α)x ∈ (⊥ : Opens α) ↔ False := Iff.rfl

Empty Set Membership in Open Sets Lattice is False

Informal description

For any point $x$ in a topological space $\alpha$, the statement that $x$ belongs to the bottom element of the lattice of open sets (the empty set) is equivalent to false.

TopologicalSpace.Opens.mk_empty theorem

: (⟨∅, isOpen_empty⟩ : Opens α) = ⊥

Full source

@[simp] theorem mk_empty : (⟨∅, isOpen_empty⟩ : Opens α) = ⊥ := rfl

Empty Set as Bottom Element in Lattice of Open Sets

Informal description

The open set constructed from the empty set in a topological space $\alpha$ is equal to the bottom element of the lattice of open sets, i.e., $\langle \emptyset, \text{isOpen\_empty} \rangle = \bot$.

TopologicalSpace.Opens.coe_eq_empty theorem

{U : Opens α} : (U : Set α) = ∅ ↔ U = ⊥

Full source

@[simp, norm_cast]
theorem coe_eq_empty {U : Opens α} : (U : Set α) = ∅ ↔ U = ⊥ :=
  SetLike.coe_injective.eq_iff' rfl

Empty Open Set Characterization: $U = \emptyset \leftrightarrow U = \bot$

Informal description

For any open subset $U$ of a topological space $\alpha$, the underlying set of $U$ is empty if and only if $U$ is the bottom element of the complete lattice of open sets (i.e., the empty open set).

TopologicalSpace.Opens.mem_top theorem

(x : α) : x ∈ (⊤ : Opens α)

Full source

@[simp]
lemma mem_top (x : α) : x ∈ (⊤ : Opens α) := trivial

Every Point Belongs to the Maximal Open Set

Informal description

For any point $x$ in a topological space $\alpha$, $x$ belongs to the maximal open subset $\top$ of $\alpha$.

TopologicalSpace.Opens.coe_top theorem

: ((⊤ : Opens α) : Set α) = Set.univ

Full source

@[simp, norm_cast]
theorem coe_top : ((⊤ : Opens α) : Set α) = Set.univ :=
  rfl

Top Open Set Equals Universal Set

Informal description

The underlying set of the top element in the lattice of open subsets of a topological space $\alpha$ is equal to the universal set $\alpha$, i.e., $(\top : \text{Opens } \alpha) = \text{univ}$.

TopologicalSpace.Opens.mk_univ theorem

: (⟨univ, isOpen_univ⟩ : Opens α) = ⊤

Full source

@[simp] theorem mk_univ : (⟨univ, isOpen_univ⟩ : Opens α) = ⊤ := rfl

Universal Set as Top Element in Lattice of Open Sets

Informal description

The open subset of a topological space $\alpha$ consisting of the entire space (i.e., the set $\alpha$ itself with the proof that it is open) is equal to the top element in the complete lattice of open subsets of $\alpha$.

TopologicalSpace.Opens.coe_eq_univ theorem

{U : Opens α} : (U : Set α) = univ ↔ U = ⊤

Full source

@[simp, norm_cast]
theorem coe_eq_univ {U : Opens α} : (U : Set α) = univ ↔ U = ⊤ :=
  SetLike.coe_injective.eq_iff' rfl

Characterization of the Top Open Set via Underlying Set

Informal description

For any open subset $U$ of a topological space $\alpha$, the underlying set of $U$ is equal to the entire space $\alpha$ if and only if $U$ is the top element in the complete lattice of open sets.

TopologicalSpace.Opens.coe_sSup theorem

{S : Set (Opens α)} : (↑(sSup S) : Set α) = ⋃ i ∈ S, ↑i

Full source

@[simp, norm_cast]
theorem coe_sSup {S : Set (Opens α)} : (↑(sSup S) : Set α) = ⋃ i ∈ S, ↑i :=
  rfl

Supremum of Open Sets as Union of Their Underlying Sets

Informal description

For any collection $S$ of open subsets of a topological space $\alpha$, the underlying set of the supremum of $S$ in the complete lattice of open sets is equal to the union of all the underlying sets of the elements in $S$. In other words, if we denote the coercion from open sets to sets by $U \mapsto \overline{U}$, then $\overline{\bigsqcup S} = \bigcup_{i \in S} \overline{i}$.

TopologicalSpace.Opens.coe_finset_sup theorem

(f : ι → Opens α) (s : Finset ι) : (↑(s.sup f) : Set α) = s.sup ((↑) ∘ f)

Full source

@[simp, norm_cast]
theorem coe_finset_sup (f : ι → Opens α) (s : Finset ι) : (↑(s.sup f) : Set α) = s.sup ((↑) ∘ f) :=
  map_finset_sup (⟨⟨(↑), coe_sup⟩, coe_bot⟩ : SupBotHom (Opens α) (Set α)) _ _

Finite Supremum of Open Sets as Union of Underlying Sets

Informal description

For any finite set $s$ of indices and any family of open sets $f : \iota \to \text{Opens}(\alpha)$, the underlying set of the supremum of $f$ over $s$ is equal to the pointwise supremum of the underlying sets of $f$ over $s$. That is, \[ \left( \bigsqcup_{i \in s} f(i) \right) = \bigcup_{i \in s} f(i) \] where $\bigsqcup$ denotes the supremum in the lattice of open sets and $\bigcup$ denotes the union of sets.

TopologicalSpace.Opens.coe_finset_inf theorem

(f : ι → Opens α) (s : Finset ι) : (↑(s.inf f) : Set α) = s.inf ((↑) ∘ f)

Full source

@[simp, norm_cast]
theorem coe_finset_inf (f : ι → Opens α) (s : Finset ι) : (↑(s.inf f) : Set α) = s.inf ((↑) ∘ f) :=
  map_finset_inf (⟨⟨(↑), coe_inf⟩, coe_top⟩ : InfTopHom (Opens α) (Set α)) _ _

Finite Infimum of Open Sets as Intersection of Their Underlying Sets

Informal description

For any finite set $s$ of indices and any family of open sets $f : \iota \to \text{Opens}(\alpha)$, the underlying set of the infimum of $f$ over $s$ is equal to the infimum (intersection) of the underlying sets of the open sets in the family $f$ over $s$. In symbols, if we denote the coercion from open sets to sets by $U \mapsto \overline{U}$, then $\overline{\bigsqcap_{i \in s} f(i)} = \bigcap_{i \in s} \overline{f(i)}$.

TopologicalSpace.Opens.instInhabited instance

: Inhabited (Opens α)

Full source

instance : Inhabited (Opens α) := ⟨⊥⟩

Nonemptiness of Open Sets in a Topological Space

Informal description

For any topological space $\alpha$, the type of open subsets of $\alpha$ is inhabited.

TopologicalSpace.Opens.instUniqueOfIsEmpty instance

[IsEmpty α] : Unique (Opens α)

Full source

instance [IsEmpty α] : Unique (Opens α) where
  uniq _ := ext <| Subsingleton.elim _ _

Uniqueness of Open Sets in Empty Topological Spaces

Informal description

For any topological space $\alpha$ that is empty, the type of open subsets of $\alpha$ has exactly one element.

TopologicalSpace.Opens.instNontrivialOfNonempty instance

[Nonempty α] : Nontrivial (Opens α)

Full source

instance [Nonempty α] : Nontrivial (Opens α) where
  exists_pair_ne := ⟨⊥, ⊤, mt coe_inj.2 empty_ne_univ⟩

Nontriviality of Open Subsets in Nonempty Spaces

Informal description

For any nonempty topological space $\alpha$, the type of open subsets of $\alpha$ is nontrivial (i.e., contains at least two distinct elements).

TopologicalSpace.Opens.coe_iSup theorem

{ι} (s : ι → Opens α) : ((⨆ i, s i : Opens α) : Set α) = ⋃ i, s i

Full source

@[simp, norm_cast]
theorem coe_iSup {ι} (s : ι → Opens α) : ((⨆ i, s i : Opens α) : Set α) = ⋃ i, s i := by
  simp [iSup]

Supremum of Open Sets as Union

Informal description

For any family of open sets $\{U_i\}_{i \in \iota}$ in a topological space $\alpha$, the underlying set of their supremum in the complete lattice of open sets is equal to the union of the underlying sets $\bigcup_{i \in \iota} U_i$.

TopologicalSpace.Opens.iSup_def theorem

{ι} (s : ι → Opens α) : ⨆ i, s i = ⟨⋃ i, s i, isOpen_iUnion fun i => (s i).2⟩

Full source

theorem iSup_def {ι} (s : ι → Opens α) : ⨆ i, s i = ⟨⋃ i, s i, isOpen_iUnion fun i => (s i).2⟩ :=
  ext <| coe_iSup s

Supremum of Open Sets as Union of Underlying Sets

Informal description

For any family of open sets $\{U_i\}_{i \in \iota}$ in a topological space $\alpha$, the supremum $\bigsqcup_{i \in \iota} U_i$ in the complete lattice of open sets is equal to the open set whose underlying set is the union $\bigcup_{i \in \iota} U_i$ (which is open since each $U_i$ is open).

TopologicalSpace.Opens.iSup_mk theorem

 {ι} (s : ι → Set α) (h : ∀ i, IsOpen (s i)) : (⨆ i, ⟨s i, h i⟩ : Opens α) = ⟨⋃ i, s i, isOpen_iUnion h⟩

Full source

@[simp]
theorem iSup_mk {ι} (s : ι → Set α) (h : ∀ i, IsOpen (s i)) :
    (⨆ i, ⟨s i, h i⟩ : Opens α) = ⟨⋃ i, s i, isOpen_iUnion h⟩ :=
  iSup_def _

Supremum of Open Sets Constructed from a Family of Open Sets Equals Their Union

Informal description

For any family of sets $\{s_i\}_{i \in \iota}$ in a topological space $\alpha$ where each $s_i$ is open, the supremum of the corresponding family of open sets $\{\langle s_i, h_i \rangle\}_{i \in \iota}$ in the complete lattice of open sets is equal to the open set whose underlying set is the union $\bigcup_{i \in \iota} s_i$.

TopologicalSpace.Opens.mem_iSup theorem

{ι} {x : α} {s : ι → Opens α} : x ∈ iSup s ↔ ∃ i, x ∈ s i

Full source

@[simp]
theorem mem_iSup {ι} {x : α} {s : ι → Opens α} : x ∈ iSup sx ∈ iSup s ↔ ∃ i, x ∈ s i := by
  rw [← SetLike.mem_coe]
  simp

Characterization of Membership in Supremum of Open Sets

Informal description

For a topological space $\alpha$, a point $x \in \alpha$, and a family of open sets $\{U_i\}_{i \in \iota}$ in $\alpha$, the point $x$ belongs to the supremum (join) of the family $\{U_i\}$ if and only if there exists an index $i \in \iota$ such that $x \in U_i$.

TopologicalSpace.Opens.mem_sSup theorem

{Us : Set (Opens α)} {x : α} : x ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u

Full source

@[simp]
theorem mem_sSup {Us : Set (Opens α)} {x : α} : x ∈ sSup Usx ∈ sSup Us ↔ ∃ u ∈ Us, x ∈ u := by
  simp_rw [sSup_eq_iSup, mem_iSup, exists_prop]

Characterization of Membership in Supremum of Open Sets

Informal description

For a topological space $\alpha$, a point $x \in \alpha$, and a collection of open sets $U_s \subseteq \alpha$, the point $x$ belongs to the supremum (join) of $U_s$ if and only if there exists an open set $u$ in $U_s$ such that $x \in u$.

TopologicalSpace.Opens.frameMinimalAxioms definition

: Frame.MinimalAxioms (Opens α)

Full source

/-- Open sets in a topological space form a frame. -/
def frameMinimalAxioms : Frame.MinimalAxioms (Opens α) where
  inf_sSup_le_iSup_inf a s :=
    (ext <| by simp only [coe_inf, coe_iSup, coe_sSup, Set.inter_iUnion₂]).le

Frame axioms for open sets in a topological space

Informal description

The open subsets of a topological space $\alpha$ satisfy the minimal axioms of a frame, namely that for any open subset $a$ and any family of open subsets $s$, the meet of $a$ with the supremum of $s$ is less than or equal to the supremum of the meets of $a$ with each element of $s$. In other words, the following inequality holds: \[ a \cap \left( \bigcup_{i} s_i \right) \subseteq \bigcup_{i} (a \cap s_i) \]

TopologicalSpace.Opens.instFrame instance

: Frame (Opens α)

Full source

instance instFrame : Frame (Opens α) := .ofMinimalAxioms frameMinimalAxioms

The Frame Structure on Open Subsets of a Topological Space

Informal description

The open subsets of a topological space $\alpha$ form a frame, meaning they have finite meets (intersections) and arbitrary joins (unions) that satisfy the distributive law: \[ U \cap \left( \bigcup_{i} V_i \right) = \bigcup_{i} (U \cap V_i) \] for any open subset $U$ and any family of open subsets $\{V_i\}$.

TopologicalSpace.Opens.isOpenEmbedding' theorem

(U : Opens α) : IsOpenEmbedding (Subtype.val : U → α)

Full source

theorem isOpenEmbedding' (U : Opens α) : IsOpenEmbedding (Subtype.val : U → α) :=
  U.isOpen.isOpenEmbedding_subtypeVal

Inclusion of Open Subset is Open Embedding

Informal description

For any open subset $U$ of a topological space $\alpha$, the inclusion map from $U$ to $\alpha$ (given by the subtype coercion) is an open embedding.

TopologicalSpace.Opens.isOpenEmbedding_of_le theorem

{U V : Opens α} (i : U ≤ V) : IsOpenEmbedding (Set.inclusion <| SetLike.coe_subset_coe.2 i)

Full source

theorem isOpenEmbedding_of_le {U V : Opens α} (i : U ≤ V) :
    IsOpenEmbedding (Set.inclusion <| SetLike.coe_subset_coe.2 i) where
  toIsEmbedding := .inclusion i
  isOpen_range := by
    rw [Set.range_inclusion i]
    exact U.isOpen.preimage continuous_subtype_val

Inclusion of Open Subsets is Open Embedding

Informal description

For any open subsets $U$ and $V$ of a topological space $\alpha$ such that $U \subseteq V$, the inclusion map $U \hookrightarrow V$ is an open embedding.

TopologicalSpace.Opens.not_nonempty_iff_eq_bot theorem

(U : Opens α) : ¬Set.Nonempty (U : Set α) ↔ U = ⊥

Full source

theorem not_nonempty_iff_eq_bot (U : Opens α) : ¬Set.Nonempty (U : Set α)¬Set.Nonempty (U : Set α) ↔ U = ⊥ := by
  rw [← coe_inj, coe_bot, ← Set.not_nonempty_iff_eq_empty]

Empty Open Set Characterization: $U = \bot \leftrightarrow U$ is empty

Informal description

For any open subset $U$ of a topological space $\alpha$, the set $U$ is empty if and only if $U$ is equal to the bottom element (the empty open set) in the lattice of open subsets.

TopologicalSpace.Opens.ne_bot_iff_nonempty theorem

(U : Opens α) : U ≠ ⊥ ↔ Set.Nonempty (U : Set α)

Full source

theorem ne_bot_iff_nonempty (U : Opens α) : U ≠ ⊥U ≠ ⊥ ↔ Set.Nonempty (U : Set α) := by
  rw [Ne, ← not_nonempty_iff_eq_bot, not_not]

Nonempty Open Set Characterization: $U \neq \bot \leftrightarrow U$ is nonempty

Informal description

For any open subset $U$ of a topological space $\alpha$, $U$ is nonempty if and only if $U$ is not equal to the bottom element $\bot$ (the empty open set) in the lattice of open subsets.

TopologicalSpace.Opens.instIsSimpleOrderOfNonemptyOfSubsingleton instance

[Nonempty α] [Subsingleton α] : IsSimpleOrder (Opens α)

Full source

instance [Nonempty α] [Subsingleton α] : IsSimpleOrder (Opens α) where
  eq_bot_or_eq_top := eq_bot_or_top <| Subsingleton.elim _ _

Simple Order Structure on Open Sets of a Subsingleton Space

Informal description

For any nonempty topological space $\alpha$ that is a subsingleton (i.e., has at most one point), the lattice of open subsets of $\alpha$ is a simple order (i.e., has exactly two elements: the empty set and the entire space).

TopologicalSpace.Opens.IsBasis definition

(B : Set (Opens α)) : Prop

Full source

/-- A set of `opens α` is a basis if the set of corresponding sets is a topological basis. -/
def IsBasis (B : Set (Opens α)) : Prop :=
  IsTopologicalBasis (((↑) : _ → Set α) '' B)

Basis of open sets in a topological space

Informal description

A family $B$ of open subsets of a topological space $\alpha$ is called a *basis* if the collection of underlying sets of elements in $B$ forms a topological basis for $\alpha$.

TopologicalSpace.Opens.isBasis_iff_nbhd theorem

{B : Set (Opens α)} : IsBasis B ↔ ∀ {U : Opens α} {x}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U

Full source

theorem isBasis_iff_nbhd {B : Set (Opens α)} :
    IsBasisIsBasis B ↔ ∀ {U : Opens α} {x}, x ∈ U → ∃ U' ∈ B, x ∈ U' ∧ U' ≤ U := by
  constructor <;> intro h
  · rintro ⟨sU, hU⟩ x hx
    rcases h.mem_nhds_iff.mp (IsOpen.mem_nhds hU hx) with ⟨sV, ⟨⟨V, H₁, H₂⟩, hsV⟩⟩
    refine ⟨V, H₁, ?_⟩
    cases V
    dsimp at H₂
    subst H₂
    exact hsV
  · refine isTopologicalBasis_of_isOpen_of_nhds ?_ ?_
    · rintro sU ⟨U, -, rfl⟩
      exact U.2
    · intro x sU hx hsU
      rcases @h ⟨sU, hsU⟩ x hx with ⟨V, hV, H⟩
      exact ⟨V, ⟨V, hV, rfl⟩, H⟩

Neighborhood Criterion for Basis of Open Sets

Informal description

A family $B$ of open subsets of a topological space $\alpha$ forms a basis if and only if for every open set $U \subseteq \alpha$ and every point $x \in U$, there exists an open set $U' \in B$ such that $x \in U'$ and $U' \subseteq U$.

TopologicalSpace.Opens.isBasis_iff_cover theorem

{B : Set (Opens α)} : IsBasis B ↔ ∀ U : Opens α, ∃ Us, Us ⊆ B ∧ U = sSup Us

Full source

theorem isBasis_iff_cover {B : Set (Opens α)} :
    IsBasisIsBasis B ↔ ∀ U : Opens α, ∃ Us, Us ⊆ B ∧ U = sSup Us := by
  constructor
  · intro hB U
    refine ⟨{ V : Opens α | V ∈ B ∧ V ≤ U }, fun U hU => hU.left, ext ?_⟩
    rw [coe_sSup, hB.open_eq_sUnion' U.isOpen]
    simp_rw [sUnion_eq_biUnion, iUnion, mem_setOf_eq, iSup_and, iSup_image]
    rfl
  · intro h
    rw [isBasis_iff_nbhd]
    intro U x hx
    rcases h U with ⟨Us, hUs, rfl⟩
    rcases mem_sSup.1 hx with ⟨U, Us, xU⟩
    exact ⟨U, hUs Us, xU, le_sSup Us⟩

Basis Criterion: Open Sets as Suprema of Basis Elements

Informal description

A family $B$ of open subsets of a topological space $\alpha$ forms a basis if and only if every open set $U$ in $\alpha$ can be expressed as the supremum (join) of some subset $U_s \subseteq B$. In other words, $B$ is a basis precisely when any open set $U$ can be written as the union of a collection of basis elements from $B$.

TopologicalSpace.Opens.IsBasis.isCompact_open_iff_eq_finite_iUnion theorem

 {ι : Type*} (b : ι → Opens α) (hb : IsBasis (Set.range b)) (hb' : ∀ i, IsCompact (b i : Set α)) (U : Set α) :
  IsCompact U ∧ IsOpen U ↔ ∃ s : Set ι, s.Finite ∧ U = ⋃ i ∈ s, b i

Full source

/-- If `α` has a basis consisting of compact opens, then an open set in `α` is compact open iff
  it is a finite union of some elements in the basis -/
theorem IsBasis.isCompact_open_iff_eq_finite_iUnion {ι : Type*} (b : ι → Opens α)
    (hb : IsBasis (Set.range b)) (hb' : ∀ i, IsCompact (b i : Set α)) (U : Set α) :
    IsCompactIsCompact U ∧ IsOpen UIsCompact U ∧ IsOpen U ↔ ∃ s : Set ι, s.Finite ∧ U = ⋃ i ∈ s, b i := by
  apply isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis fun i : ι => (b i).1
  · convert (config := {transparency := .default}) hb
    ext
    simp
  · exact hb'

Characterization of Compact Open Sets as Finite Unions of Basis Elements

Informal description

Let $\alpha$ be a topological space with a basis $\{b_i\}_{i \in \iota}$ consisting of compact open sets. Then a subset $U \subseteq \alpha$ is compact and open if and only if there exists a finite subset $s \subseteq \iota$ such that $U = \bigcup_{i \in s} b_i$.

TopologicalSpace.Opens.IsBasis.le_iff theorem

 {α} {t₁ t₂ : TopologicalSpace α} {Us : Set (Opens α)} (hUs : @IsBasis α t₂ Us) : t₁ ≤ t₂ ↔ ∀ U ∈ Us, IsOpen[t₁] U

Full source

lemma IsBasis.le_iff {α} {t₁ t₂ : TopologicalSpace α}
    {Us : Set (Opens α)} (hUs : @IsBasis α t₂ Us) :
    t₁ ≤ t₂ ↔ ∀ U ∈ Us, IsOpen[t₁] U := by
  conv_lhs => rw [hUs.eq_generateFrom]
  simp [Set.subset_def, le_generateFrom_iff_subset_isOpen]

Basis Criterion for Comparing Topologies: $t_1 \leq t_2$ iff Basis Elements are $t_1$-open

Informal description

Let $\alpha$ be a type with two topological space structures $t_1$ and $t_2$, and let $Us$ be a set of open subsets of $\alpha$ under $t_2$ that forms a basis for $t_2$. Then $t_1$ is coarser than $t_2$ (i.e., $t_1 \leq t_2$) if and only if every open set in $Us$ is also open in $t_1$.

TopologicalSpace.Opens.isCompactElement_iff theorem

(s : Opens α) : CompleteLattice.IsCompactElement s ↔ IsCompact (s : Set α)

Full source

@[simp]
theorem isCompactElement_iff (s : Opens α) :
    CompleteLattice.IsCompactElementCompleteLattice.IsCompactElement s ↔ IsCompact (s : Set α) := by
  rw [isCompact_iff_finite_subcover, CompleteLattice.isCompactElement_iff]
  refine ⟨?_, fun H ι U hU => ?_⟩
  · introv H hU hU'
    obtain ⟨t, ht⟩ := H ι (fun i => ⟨U i, hU i⟩) (by simpa)
    refine ⟨t, Set.Subset.trans ht ?_⟩
    rw [coe_finset_sup, Finset.sup_eq_iSup]
    rfl
  · obtain ⟨t, ht⟩ :=
      H (fun i => U i) (fun i => (U i).isOpen) (by simpa using show (s : Set α) ⊆ ↑(iSup U) from hU)
    refine ⟨t, Set.Subset.trans ht ?_⟩
    simp only [Set.iUnion_subset_iff]
    show ∀ i ∈ t, U i ≤ t.sup U
    exact fun i => Finset.le_sup

Compactness in Lattice of Open Sets vs. Topological Compactness

Informal description

For any open subset $s$ of a topological space $\alpha$, $s$ is a compact element in the complete lattice of open sets if and only if the underlying set of $s$ is compact in $\alpha$.

TopologicalSpace.Opens.comap definition

(f : C(α, β)) : FrameHom (Opens β) (Opens α)

Full source

/-- The preimage of an open set, as an open set. -/
def comap (f : C(α, β)) : FrameHom (Opens β) (Opens α) where
  toFun s := ⟨f ⁻¹' s, s.2.preimage f.continuous⟩
  map_sSup' s := ext <| by simp only [coe_sSup, preimage_iUnion, biUnion_image, coe_mk]
  map_inf' _ _ := rfl
  map_top' := rfl

Preimage of open sets under a continuous map

Informal description

Given a continuous function $f \colon \alpha \to \beta$ between topological spaces, the preimage of an open set in $\beta$ under $f$ is an open set in $\alpha$. This defines a frame homomorphism from the complete lattice of open sets in $\beta$ to the complete lattice of open sets in $\alpha$.

TopologicalSpace.Opens.comap_id theorem

: comap (ContinuousMap.id α) = FrameHom.id _

Full source

@[simp]
theorem comap_id : comap (ContinuousMap.id α) = FrameHom.id _ :=
  FrameHom.ext fun _ => ext rfl

Identity Preimage Preserves Open Sets

Informal description

The preimage operation under the identity continuous map on a topological space $\alpha$ is equal to the identity frame homomorphism on the complete lattice of open subsets of $\alpha$.

TopologicalSpace.Opens.comap_mono theorem

(f : C(α, β)) {s t : Opens β} (h : s ≤ t) : comap f s ≤ comap f t

Full source

theorem comap_mono (f : C(α, β)) {s t : Opens β} (h : s ≤ t) : comap f s ≤ comap f t :=
  OrderHomClass.mono (comap f) h

Monotonicity of Preimage of Open Sets under Continuous Maps

Informal description

Let $f \colon \alpha \to \beta$ be a continuous map between topological spaces, and let $s, t$ be open subsets of $\beta$ such that $s \subseteq t$. Then the preimage of $s$ under $f$ is contained in the preimage of $t$ under $f$, i.e., $f^{-1}(s) \subseteq f^{-1}(t)$.

TopologicalSpace.Opens.coe_comap theorem

(f : C(α, β)) (U : Opens β) : ↑(comap f U) = f ⁻¹' U

Full source

@[simp]
theorem coe_comap (f : C(α, β)) (U : Opens β) : ↑(comap f U) = f ⁻¹' U :=
  rfl

Preimage of Open Set Under Continuous Function as Set

Informal description

For any continuous function $f \colon \alpha \to \beta$ between topological spaces and any open subset $U$ of $\beta$, the underlying set of the preimage of $U$ under $f$ (as an element of `Opens α`) is equal to the set-theoretic preimage $f^{-1}(U)$.

TopologicalSpace.Opens.mem_comap theorem

{f : C(α, β)} {U : Opens β} {x : α} : x ∈ comap f U ↔ f x ∈ U

Full source

@[simp]
theorem mem_comap {f : C(α, β)} {U : Opens β} {x : α} : x ∈ comap f Ux ∈ comap f U ↔ f x ∈ U := .rfl

Characterization of Points in Preimage of Open Set under Continuous Map

Informal description

Let $f \colon \alpha \to \beta$ be a continuous map between topological spaces, $U$ be an open subset of $\beta$, and $x$ be a point in $\alpha$. Then $x$ belongs to the preimage of $U$ under $f$ if and only if $f(x)$ belongs to $U$. In other words, $x \in f^{-1}(U) \leftrightarrow f(x) \in U$.

TopologicalSpace.Opens.comap_comp theorem

(g : C(β, γ)) (f : C(α, β)) : comap (g.comp f) = (comap f).comp (comap g)

Full source

protected theorem comap_comp (g : C(β, γ)) (f : C(α, β)) :
    comap (g.comp f) = (comap f).comp (comap g) :=
  rfl

Composition Property of Preimages of Open Sets under Continuous Maps

Informal description

For continuous functions $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ between topological spaces, the preimage operation satisfies the composition property: \[ \text{comap}(g \circ f) = \text{comap}(f) \circ \text{comap}(g) \] where $\text{comap}(f) \colon \text{Opens}(\beta) \to \text{Opens}(\alpha)$ denotes the frame homomorphism that takes preimages under $f$.

TopologicalSpace.Opens.comap_comap theorem

(g : C(β, γ)) (f : C(α, β)) (U : Opens γ) : comap f (comap g U) = comap (g.comp f) U

Full source

protected theorem comap_comap (g : C(β, γ)) (f : C(α, β)) (U : Opens γ) :
    comap f (comap g U) = comap (g.comp f) U :=
  rfl

Composition Law for Preimages of Open Sets: $(g \circ f)^{-1}(U) = f^{-1}(g^{-1}(U))$

Informal description

Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be continuous maps between topological spaces. For any open set $U \subseteq \gamma$, the preimage of $U$ under the composition $g \circ f$ equals the preimage under $f$ of the preimage of $U$ under $g$. In other words, $(g \circ f)^{-1}(U) = f^{-1}(g^{-1}(U))$ as open sets in $\alpha$.

TopologicalSpace.Opens.comap_injective theorem

[T0Space β] : Injective (comap : C(α, β) → FrameHom (Opens β) (Opens α))

Full source

theorem comap_injective [T0Space β] : Injective (comap : C(α, β) → FrameHom (Opens β) (Opens α)) :=
  fun f g h =>
  ContinuousMap.ext fun a =>
    Inseparable.eq <|
      inseparable_iff_forall_isOpen.2 fun s hs =>
        have : comap f ⟨s, hs⟩ = comap g ⟨s, hs⟩ := DFunLike.congr_fun h ⟨_, hs⟩
        show a ∈ f ⁻¹' sa ∈ f ⁻¹' s ↔ a ∈ g ⁻¹' s from Set.ext_iff.1 (coe_inj.2 this) a

Injectivity of Open Set Preimage Map in T₀ Spaces

Informal description

Let $\alpha$ and $\beta$ be topological spaces, with $\beta$ being a T₀ space. Then the preimage map $\text{comap} : C(\alpha, \beta) \to \text{FrameHom}(\text{Opens}(\beta), \text{Opens}(\alpha))$, which sends a continuous function to its induced frame homomorphism on open sets, is injective.

Homeomorph.opensCongr definition

(f : α ≃ₜ β) : Opens α ≃o Opens β

Full source

/-- A homeomorphism induces an order-preserving equivalence on open sets, by taking comaps. -/
@[simps -fullyApplied apply]
def _root_.Homeomorph.opensCongr (f : α ≃ₜ β) : OpensOpens α ≃o Opens β where
  toFun := Opens.comap (f.symm : C(β, α))
  invFun := Opens.comap (f : C(α, β))
  left_inv _ := ext <| f.toEquiv.preimage_symm_preimage _
  right_inv _ := ext <| f.toEquiv.symm_preimage_preimage _
  map_rel_iff' := by
    simp only [← SetLike.coe_subset_coe]; exact f.symm.surjective.preimage_subset_preimage_iff

Order-preserving equivalence of open sets induced by a homeomorphism

Informal description

Given a homeomorphism $f \colon \alpha \simeq \beta$ between topological spaces, the function `Homeomorph.opensCongr` establishes an order-preserving equivalence between the complete lattices of open sets in $\alpha$ and $\beta$. Specifically, it maps an open set $U \subseteq \alpha$ to its preimage under $f^{-1} \colon \beta \to \alpha$, and vice versa, preserving the inclusion order.

Homeomorph.opensCongr_symm theorem

(f : α ≃ₜ β) : f.opensCongr.symm = f.symm.opensCongr

Full source

@[simp]
theorem _root_.Homeomorph.opensCongr_symm (f : α ≃ₜ β) : f.opensCongr.symm = f.symm.opensCongr :=
  rfl

Inverse of Open Set Equivalence Induced by Homeomorphism

Informal description

For any homeomorphism $f \colon \alpha \simeq \beta$ between topological spaces, the inverse of the order-preserving equivalence $f.opensCongr \colon \text{Opens}(\alpha) \simeq_o \text{Opens}(\beta)$ is equal to the order-preserving equivalence induced by the inverse homeomorphism $f.symm.opensCongr \colon \text{Opens}(\beta) \simeq_o \text{Opens}(\alpha)$.

TopologicalSpace.Opens.instFinite instance

[Finite α] : Finite (Opens α)

Full source

instance [Finite α] : Finite (Opens α) :=
  Finite.of_injective _ SetLike.coe_injective

Finiteness of Open Sets in Finite Topological Spaces

Informal description

For any finite topological space $\alpha$, the type of open subsets of $\alpha$ is finite.

TopologicalSpace.OpenNhdsOf structure

(x : α) extends Opens α

Full source

/-- The open neighborhoods of a point. See also `Opens` or `nhds`. -/
structure OpenNhdsOf (x : α) extends Opens α where
  /-- The point `x` belongs to every `U : TopologicalSpace.OpenNhdsOf x`. -/
  mem' : x ∈ carrier

Open neighborhoods of a point in a topological space

Informal description

The structure representing the open neighborhoods of a point $ x $ in a topological space $ \alpha $. It extends the type of open sets in $ \alpha $ and consists of all open subsets of $ \alpha $ that contain $ x $.

TopologicalSpace.OpenNhdsOf.toOpens_injective theorem

: Injective (toOpens : OpenNhdsOf x → Opens α)

Full source

theorem toOpens_injective : Injective (toOpens : OpenNhdsOf x → Opens α)
  | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

Injectivity of the Open Neighborhoods to Open Sets Map

Informal description

The canonical map from the type of open neighborhoods of a point $x$ in a topological space $\alpha$ to the type of open subsets of $\alpha$ is injective. In other words, if two open neighborhoods of $x$ have the same underlying open set, then they are equal.

TopologicalSpace.OpenNhdsOf.instSetLike instance

: SetLike (OpenNhdsOf x) α

Full source

instance : SetLike (OpenNhdsOf x) α where
  coe U := U.1
  coe_injective' := SetLike.coe_injective.comp toOpens_injective

Open Neighborhoods as Sets in a Topological Space

Informal description

The type of open neighborhoods of a point $x$ in a topological space $\alpha$ is equipped with a `SetLike` structure, allowing its elements to be treated as sets of elements of $\alpha$.

TopologicalSpace.OpenNhdsOf.canLiftSet instance

: CanLift (Set α) (OpenNhdsOf x) (↑) fun s => IsOpen s ∧ x ∈ s

Full source

instance canLiftSet : CanLift (Set α) (OpenNhdsOf x) (↑) fun s => IsOpenIsOpen s ∧ x ∈ s :=
  ⟨fun s hs => ⟨⟨⟨s, hs.1⟩, hs.2⟩, rfl⟩⟩

Lifting Condition for Open Neighborhoods of a Point

Informal description

Given a topological space $\alpha$ and a point $x \in \alpha$, there exists a lifting condition from sets in $\alpha$ to open neighborhoods of $x$, where a set $s$ can be lifted to an open neighborhood of $x$ if and only if $s$ is open and contains $x$.

TopologicalSpace.OpenNhdsOf.mem theorem

(U : OpenNhdsOf x) : x ∈ U

Full source

protected theorem mem (U : OpenNhdsOf x) : x ∈ U :=
  U.mem'

Membership in Open Neighborhoods

Informal description

For any open neighborhood $U$ of a point $x$ in a topological space $\alpha$, the point $x$ belongs to $U$.

TopologicalSpace.OpenNhdsOf.isOpen theorem

(U : OpenNhdsOf x) : IsOpen (U : Set α)

Full source

protected theorem isOpen (U : OpenNhdsOf x) : IsOpen (U : Set α) :=
  U.is_open'

Openness of Neighborhoods in a Topological Space

Informal description

For any open neighborhood $U$ of a point $x$ in a topological space $\alpha$, the underlying set $U$ is open in $\alpha$.

TopologicalSpace.OpenNhdsOf.instOrderTop instance

: OrderTop (OpenNhdsOf x)

Full source

instance : OrderTop (OpenNhdsOf x) where
  top := ⟨⊤, Set.mem_univ _⟩
  le_top _ := subset_univ _

Order with Top Element on Open Neighborhoods

Informal description

The collection of open neighborhoods of a point $x$ in a topological space $\alpha$ forms an order with a top element, where the order is given by inclusion and the top element is the entire space $\alpha$.

TopologicalSpace.OpenNhdsOf.instInhabited instance

: Inhabited (OpenNhdsOf x)

Full source

instance : Inhabited (OpenNhdsOf x) := ⟨⊤⟩

Nonemptiness of Open Neighborhoods of a Point

Informal description

For any point $x$ in a topological space $\alpha$, the type of open neighborhoods of $x$ is inhabited.

TopologicalSpace.OpenNhdsOf.instMin instance

: Min (OpenNhdsOf x)

Full source

instance : Min (OpenNhdsOf x) := ⟨fun U V => ⟨U.1 ⊓ V.1, U.2, V.2⟩⟩

Minimum Operation on Open Neighborhoods of a Point

Informal description

For any point $x$ in a topological space $\alpha$, the type of open neighborhoods of $x$ has a minimum operation with respect to the inclusion order.

TopologicalSpace.OpenNhdsOf.instMax instance

: Max (OpenNhdsOf x)

Full source

instance : Max (OpenNhdsOf x) := ⟨fun U V => ⟨U.1 ⊔ V.1, Or.inl U.2⟩⟩

Existence of Maximal Open Neighborhood

Informal description

For any point $x$ in a topological space $\alpha$, the type of open neighborhoods of $x$ has a maximal element.

TopologicalSpace.OpenNhdsOf.instUniqueOfSubsingleton instance

[Subsingleton α] : Unique (OpenNhdsOf x)

Full source

instance [Subsingleton α] : Unique (OpenNhdsOf x) where
  uniq U := SetLike.ext' <| Subsingleton.eq_univ_of_nonempty ⟨x, U.mem⟩

Uniqueness of Open Neighborhoods in Subsingleton Spaces

Informal description

For any topological space $\alpha$ that is a subsingleton (i.e., has at most one point), the type of open neighborhoods of any point $x$ in $\alpha$ is uniquely determined.

TopologicalSpace.OpenNhdsOf.instDistribLattice instance

: DistribLattice (OpenNhdsOf x)

Full source

instance : DistribLattice (OpenNhdsOf x) :=
  toOpens_injective.distribLattice _ (fun _ _ => rfl) fun _ _ => rfl

Distributive Lattice Structure on Open Neighborhoods of a Point

Informal description

For any point $x$ in a topological space $\alpha$, the open neighborhoods of $x$ form a distributive lattice under the inclusion order.

TopologicalSpace.OpenNhdsOf.basis_nhds theorem

: (𝓝 x).HasBasis (fun _ : OpenNhdsOf x => True) (↑)

Full source

theorem basis_nhds : (𝓝 x).HasBasis (fun _ : OpenNhdsOf x => True) (↑) :=
  (nhds_basis_opens x).to_hasBasis (fun U hU => ⟨⟨⟨U, hU.2⟩, hU.1⟩, trivial, Subset.rfl⟩) fun U _ =>
    ⟨U, ⟨⟨U.mem, U.isOpen⟩, Subset.rfl⟩⟩

Open Neighborhoods Form Basis for Neighborhood Filter

Informal description

The open neighborhoods of a point $x$ in a topological space $\alpha$ form a basis for the neighborhood filter $\mathcal{N}(x)$, where each open neighborhood $U$ of $x$ (i.e., $U$ is an open set containing $x$) satisfies the trivial condition `True` and is represented by its underlying set $U \subseteq \alpha$.

TopologicalSpace.OpenNhdsOf.comap definition

(f : C(α, β)) (x : α) : LatticeHom (OpenNhdsOf (f x)) (OpenNhdsOf x)

Full source

/-- Preimage of an open neighborhood of `f x` under a continuous map `f` as a `LatticeHom`. -/
def comap (f : C(α, β)) (x : α) : LatticeHom (OpenNhdsOf (f x)) (OpenNhdsOf x) where
  toFun U := ⟨Opens.comap f U.1, U.mem⟩
  map_sup' _ _ := rfl
  map_inf' _ _ := rfl

Preimage of open neighborhoods under a continuous map as a lattice homomorphism

Informal description

Given a continuous function $ f \colon \alpha \to \beta $ between topological spaces and a point $ x \in \alpha $, the function maps an open neighborhood $ U $ of $ f(x) $ to its preimage $ f^{-1}(U) $, which is an open neighborhood of $ x $. This defines a lattice homomorphism between the lattice of open neighborhoods of $ f(x) $ and the lattice of open neighborhoods of $ x $, preserving both finite suprema (unions) and finite infima (intersections).

Mathlib.Topology.Sets.Opens

Summary

Main Definitions

Bundled open sets

Bundled open neighborhoods

Main results

TODO