Mathlib.Topology.Order

TopologicalSpace.GenerateOpen inductive

(g : Set (Set α)) : Set α → Prop

Full source

/-- The open sets of the least topology containing a collection of basic sets. -/
inductive GenerateOpen (g : Set (Set α)) : Set α → Prop
  | basic : ∀ s ∈ g, GenerateOpen g s
  | univ : GenerateOpen g univ
  | inter : ∀ s t, GenerateOpen g s → GenerateOpen g t → GenerateOpen g (s ∩ t)
  | sUnion : ∀ S : Set (Set α), (∀ s ∈ S, GenerateOpen g s) → GenerateOpen g (⋃₀ S)

Generated open sets of a topology

Informal description

The inductive predicate `TopologicalSpace.GenerateOpen g` defines the open sets of the least topology on a type `α` containing a given collection of basic open sets `g`. Here, `g` is a family of subsets of `α`. The predicate holds for a set `s` if `s` can be generated from the sets in `g` through finite intersections and arbitrary unions.

TopologicalSpace.generateFrom definition

(g : Set (Set α)) : TopologicalSpace α

Full source

/-- The smallest topological space containing the collection `g` of basic sets -/
def generateFrom (g : Set (Set α)) : TopologicalSpace α where
  IsOpen := GenerateOpen g
  isOpen_univ := GenerateOpen.univ
  isOpen_inter := GenerateOpen.inter
  isOpen_sUnion := GenerateOpen.sUnion

Topology generated by a collection of sets

Informal description

The topology generated from a collection of basic open sets $g$ is the smallest topology on $\alpha$ containing all sets in $g$. A set is open in this topology if it can be obtained from the sets in $g$ through finite intersections and arbitrary unions.

TopologicalSpace.isOpen_generateFrom_of_mem theorem

{g : Set (Set α)} {s : Set α} (hs : s ∈ g) : IsOpen[generateFrom g] s

Full source

theorem isOpen_generateFrom_of_mem {g : Set (Set α)} {s : Set α} (hs : s ∈ g) :
    IsOpen[generateFrom g] s :=
  GenerateOpen.basic s hs

Basic Sets are Open in Generated Topology

Informal description

For any collection of subsets $g$ of a type $\alpha$ and any subset $s \in g$, the set $s$ is open in the topology generated by $g$.

TopologicalSpace.nhds_generateFrom theorem

{g : Set (Set α)} {a : α} : @nhds α (generateFrom g) a = ⨅ s ∈ {s | a ∈ s ∧ s ∈ g}, 𝓟 s

Full source

theorem nhds_generateFrom {g : Set (Set α)} {a : α} :
    @nhds α (generateFrom g) a = ⨅ s ∈ { s | a ∈ s ∧ s ∈ g }, 𝓟 s := by
  letI := generateFrom g
  rw [nhds_def]
  refine le_antisymm (biInf_mono fun s ⟨as, sg⟩ => ⟨as, .basic _ sg⟩) <| le_iInf₂ ?_
  rintro s ⟨ha, hs⟩
  induction hs with
  | basic _ hs => exact iInf₂_le _ ⟨ha, hs⟩
  | univ => exact le_top.trans_eq principal_univ.symm
  | inter _ _ _ _ hs ht => exact (le_inf (hs ha.1) (ht ha.2)).trans_eq inf_principal
  | sUnion _ _ hS =>
    let ⟨t, htS, hat⟩ := ha
    exact (hS t htS hat).trans (principal_mono.2 <| subset_sUnion_of_mem htS)

Neighborhood Filter in Generated Topology as Infimum of Principal Filters

Informal description

For any collection of sets $g$ in a type $\alpha$ and any point $a \in \alpha$, the neighborhood filter of $a$ in the topology generated by $g$ is equal to the infimum of the principal filters of all sets $s \in g$ that contain $a$. In other words, \[ \text{nhds}(a) = \bigsqcap_{\substack{s \in g \\ a \in s}} \text{principal}(s), \] where $\text{nhds}(a)$ is the neighborhood filter of $a$ in the generated topology, and $\text{principal}(s)$ is the principal filter generated by the set $s$.

TopologicalSpace.tendsto_nhds_generateFrom_iff theorem

 {β : Type*} {m : α → β} {f : Filter α} {g : Set (Set β)} {b : β} :
  Tendsto m f (@nhds β (generateFrom g) b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f

Full source

lemma tendsto_nhds_generateFrom_iff {β : Type*} {m : α → β} {f : Filter α} {g : Set (Set β)}
    {b : β} : TendstoTendsto m f (@nhds β (generateFrom g) b) ↔ ∀ s ∈ g, b ∈ s → m ⁻¹' s ∈ f := by
  simp only [nhds_generateFrom, @forall_swap (b ∈ _), tendsto_iInf, mem_setOf_eq, and_imp,
    tendsto_principal]; rfl

Characterization of Convergence in Generated Topology via Basic Open Sets

Informal description

Let $\alpha$ and $\beta$ be types, $m : \alpha \to \beta$ a function, $f$ a filter on $\alpha$, $g$ a collection of subsets of $\beta$, and $b \in \beta$. Then the following are equivalent: 1. The function $m$ tends to the neighborhood filter of $b$ in the topology generated by $g$ along $f$. 2. For every set $s \in g$ containing $b$, the preimage $m^{-1}(s)$ belongs to the filter $f$.

TopologicalSpace.mkOfNhds definition

(n : α → Filter α) : TopologicalSpace α

Full source

/-- Construct a topology on α given the filter of neighborhoods of each point of α. -/
protected def mkOfNhds (n : α → Filter α) : TopologicalSpace α where
  IsOpen s := ∀ a ∈ s, s ∈ n a
  isOpen_univ _ _ := univ_mem
  isOpen_inter := fun _s _t hs ht x ⟨hxs, hxt⟩ => inter_mem (hs x hxs) (ht x hxt)
  isOpen_sUnion := fun _s hs _a ⟨x, hx, hxa⟩ =>
    mem_of_superset (hs x hx _ hxa) (subset_sUnion_of_mem hx)

Topology generated by neighborhood filters

Informal description

Given a function `n : α → Filter α` that assigns to each point `a : α` a filter of neighborhoods, the topology `TopologicalSpace.mkOfNhds n` on `α` is defined by declaring a set `s` to be open if for every point `a ∈ s`, the set `s` belongs to the neighborhood filter `n a`. This construction ensures that the topology is generated by the given neighborhood filters.

TopologicalSpace.nhds_mkOfNhds_of_hasBasis theorem

 {n : α → Filter α} {ι : α → Sort*} {p : ∀ a, ι a → Prop} {s : ∀ a, ι a → Set α} (hb : ∀ a, (n a).HasBasis (p a) (s a))
  (hpure : ∀ a i, p a i → a ∈ s a i) (hopen : ∀ a i, p a i → ∀ᶠ x in n a, s a i ∈ n x) (a : α) :
  @nhds α (.mkOfNhds n) a = n a

Full source

theorem nhds_mkOfNhds_of_hasBasis {n : α → Filter α} {ι : α → Sort*} {p : ∀ a, ι a → Prop}
    {s : ∀ a, ι a → Set α} (hb : ∀ a, (n a).HasBasis (p a) (s a))
    (hpure : ∀ a i, p a i → a ∈ s a i) (hopen : ∀ a i, p a i → ∀ᶠ x in n a, s a i ∈ n x) (a : α) :
    @nhds α (.mkOfNhds n) a = n a := by
  let t : TopologicalSpace α := .mkOfNhds n
  apply le_antisymm
  · intro U hU
    replace hpure : pure ≤ n := fun x ↦ (hb x).ge_iff.2 (hpure x)
    refine mem_nhds_iff.2 ⟨{x | U ∈ n x}, fun x hx ↦ hpure x hx, fun x hx ↦ ?_, hU⟩
    rcases (hb x).mem_iff.1 hx with ⟨i, hpi, hi⟩
    exact (hopen x i hpi).mono fun y hy ↦ mem_of_superset hy hi
  · exact (nhds_basis_opens a).ge_iff.2 fun U ⟨haU, hUo⟩ ↦ hUo a haU

Neighborhood Filter in Generated Topology via Basis

Informal description

Let $\alpha$ be a type and $n : \alpha \to \text{Filter } \alpha$ a function assigning to each point $a \in \alpha$ a filter of neighborhoods. Suppose that for each $a \in \alpha$, the filter $n(a)$ has a basis indexed by $\iota(a)$ with predicate $p(a)$ and sets $s(a,i) \subseteq \alpha$ (i.e., $n(a)$ is generated by $\{s(a,i) \mid i \in \iota(a), p(a,i)\}$). Assume further that: 1. For all $a \in \alpha$ and $i \in \iota(a)$, if $p(a,i)$ holds, then $a \in s(a,i)$. 2. For all $a \in \alpha$ and $i \in \iota(a)$, if $p(a,i)$ holds, then $s(a,i)$ is eventually in $n(x)$ for $x$ in $n(a)$. Then, for any $a \in \alpha$, the neighborhood filter of $a$ in the topology generated by $n$ (via `TopologicalSpace.mkOfNhds`) coincides with $n(a)$. That is, $\mathcal{N}_{\text{mkOfNhds } n}(a) = n(a)$.

TopologicalSpace.nhds_mkOfNhds theorem

 (n : α → Filter α) (a : α) (h₀ : pure ≤ n) (h₁ : ∀ a, ∀ s ∈ n a, ∀ᶠ y in n a, s ∈ n y) :
  @nhds α (TopologicalSpace.mkOfNhds n) a = n a

Full source

theorem nhds_mkOfNhds (n : α → Filter α) (a : α) (h₀ : pure ≤ n)
    (h₁ : ∀ a, ∀ s ∈ n a, ∀ᶠ y in n a, s ∈ n y) :
    @nhds α (TopologicalSpace.mkOfNhds n) a = n a :=
  nhds_mkOfNhds_of_hasBasis (fun a ↦ (n a).basis_sets) h₀ h₁ _

Neighborhood Filter in Generated Topology via Neighborhood Function

Informal description

Let $\alpha$ be a type and $n : \alpha \to \text{Filter } \alpha$ a function assigning to each point $a \in \alpha$ a filter of neighborhoods. Suppose that: 1. For every $a \in \alpha$, the pure filter (generated by $\{a\}$) is contained in $n(a)$. 2. For every $a \in \alpha$ and every set $s$ in the neighborhood filter $n(a)$, the set $s$ is eventually in the neighborhood filter $n(y)$ for $y$ in $n(a)$. Then, for any $a \in \alpha$, the neighborhood filter of $a$ in the topology generated by $n$ (via `TopologicalSpace.mkOfNhds`) coincides with $n(a)$. That is, $\mathcal{N}_{\text{mkOfNhds } n}(a) = n(a)$.

TopologicalSpace.nhds_mkOfNhds_single theorem

 [DecidableEq α] {a₀ : α} {l : Filter α} (h : pure a₀ ≤ l) (b : α) :
  @nhds α (TopologicalSpace.mkOfNhds (update pure a₀ l)) b = (update pure a₀ l : α → Filter α) b

Full source

theorem nhds_mkOfNhds_single [DecidableEq α] {a₀ : α} {l : Filter α} (h : pure a₀ ≤ l) (b : α) :
    @nhds α (TopologicalSpace.mkOfNhds (update pure a₀ l)) b =
      (update pure a₀ l : α → Filter α) b := by
  refine nhds_mkOfNhds _ _ (le_update_iff.mpr ⟨h, fun _ _ => le_rfl⟩) fun a s hs => ?_
  rcases eq_or_ne a a₀ with (rfl | ha)
  · filter_upwards [hs] with b hb
    rcases eq_or_ne b a with (rfl | hb)
    · exact hs
    · rwa [update_of_ne hb]
  · simpa only [update_of_ne ha, mem_pure, eventually_pure] using hs

Neighborhood Filter in Point-Updated Topology

Informal description

Let $\alpha$ be a type with decidable equality, $a_0 \in \alpha$ a distinguished point, and $l$ a filter on $\alpha$ such that the principal filter $\{a_0\}$ is contained in $l$. Then for any point $b \in \alpha$, the neighborhood filter of $b$ in the topology generated by the function that maps $a_0$ to $l$ and all other points to their principal filters, is equal to the updated filter function evaluated at $b$. In other words, if we define a neighborhood function $n : \alpha \to \text{Filter } \alpha$ where $n(a_0) = l$ and $n(a) = \{a\}$ for $a \neq a_0$, then the neighborhood filter at any point $b$ in the generated topology coincides with $n(b)$.

TopologicalSpace.nhds_mkOfNhds_filterBasis theorem

 (B : α → FilterBasis α) (a : α) (h₀ : ∀ x, ∀ n ∈ B x, x ∈ n)
  (h₁ : ∀ x, ∀ n ∈ B x, ∃ n₁ ∈ B x, ∀ x' ∈ n₁, ∃ n₂ ∈ B x', n₂ ⊆ n) :
  @nhds α (TopologicalSpace.mkOfNhds fun x => (B x).filter) a = (B a).filter

Full source

theorem nhds_mkOfNhds_filterBasis (B : α → FilterBasis α) (a : α) (h₀ : ∀ x, ∀ n ∈ B x, x ∈ n)
    (h₁ : ∀ x, ∀ n ∈ B x, ∃ n₁ ∈ B x, ∀ x' ∈ n₁, ∃ n₂ ∈ B x', n₂ ⊆ n) :
    @nhds α (TopologicalSpace.mkOfNhds fun x => (B x).filter) a = (B a).filter :=
  nhds_mkOfNhds_of_hasBasis (fun a ↦ (B a).hasBasis) h₀ h₁ a

Neighborhood Filter in Generated Topology via Filter Bases

Informal description

Let $\alpha$ be a type and $B : \alpha \to \text{FilterBasis } \alpha$ a function assigning to each point $x \in \alpha$ a filter basis $B(x)$. Suppose that: 1. For every $x \in \alpha$ and every $n \in B(x)$, the point $x$ belongs to $n$. 2. For every $x \in \alpha$ and every $n \in B(x)$, there exists $n_1 \in B(x)$ such that for every $x' \in n_1$, there exists $n_2 \in B(x')$ with $n_2 \subseteq n$. Then, for any $a \in \alpha$, the neighborhood filter of $a$ in the topology generated by the filter bases $B$ (via `TopologicalSpace.mkOfNhds`) coincides with the filter generated by $B(a)$. That is, $\mathcal{N}_{\text{mkOfNhds } (\lambda x, (B x).\text{filter})}(a) = (B a).\text{filter}$.

TopologicalSpace.instPartialOrder instance

: PartialOrder (TopologicalSpace α)

Full source

/-- The ordering on topologies on the type `α`. `t ≤ s` if every set open in `s` is also open in `t`
(`t` is finer than `s`). -/
instance : PartialOrder (TopologicalSpace α) :=
  { PartialOrder.lift (fun t => OrderDual.toDual IsOpen[t]) (fun _ _ => TopologicalSpace.ext) with
    le := fun s t => ∀ U, IsOpen[t] U → IsOpen[s] U }

Partial Order on Topological Spaces by Fineness

Informal description

For any type $\alpha$, the collection of all topological spaces on $\alpha$ forms a partial order under the relation of fineness. Specifically, for two topological spaces $t$ and $s$ on $\alpha$, we say $t \leq s$ if every open set in $s$ is also open in $t$ (i.e., $t$ is finer than $s$).

TopologicalSpace.le_def theorem

{α} {t s : TopologicalSpace α} : t ≤ s ↔ IsOpen[s] ≤ IsOpen[t]

Full source

protected theorem le_def {α} {t s : TopologicalSpace α} : t ≤ s ↔ IsOpen[s] ≤ IsOpen[t] :=
  Iff.rfl

Fineness Criterion for Topological Spaces: $t \leq s$ iff Open Sets in $s$ are Open in $t$

Informal description

For any two topological spaces $t$ and $s$ on a type $\alpha$, the relation $t \leq s$ holds if and only if every set that is open in $s$ is also open in $t$. In other words, $t$ is finer than $s$ precisely when the collection of open sets in $s$ is a subset of the collection of open sets in $t$.

TopologicalSpace.le_generateFrom_iff_subset_isOpen theorem

{g : Set (Set α)} {t : TopologicalSpace α} : t ≤ generateFrom g ↔ g ⊆ {s | IsOpen[t] s}

Full source

theorem le_generateFrom_iff_subset_isOpen {g : Set (Set α)} {t : TopologicalSpace α} :
    t ≤ generateFrom g ↔ g ⊆ { s | IsOpen[t] s } :=
  ⟨fun ht s hs => ht _ <| .basic s hs, fun hg _s hs =>
    hs.recOn (fun _ h => hg h) isOpen_univ (fun _ _ _ _ => IsOpen.inter) fun _ _ => isOpen_sUnion⟩

Fineness Criterion for Generated Topology: $t \leq \text{generateFrom } g$ iff $g$ is Open in $t$

Informal description

For any collection of sets $g$ in a type $\alpha$ and any topological space $t$ on $\alpha$, the topology $t$ is finer than the topology generated by $g$ if and only if every set in $g$ is open in $t$. In other words, $t \leq \text{generateFrom } g$ holds precisely when $g \subseteq \{s \mid \text{IsOpen}[t] s\}$.

TopologicalSpace.mkOfClosure definition

(s : Set (Set α)) (hs : {u | GenerateOpen s u} = s) : TopologicalSpace α

Full source

/-- If `s` equals the collection of open sets in the topology it generates, then `s` defines a
topology. -/
protected def mkOfClosure (s : Set (Set α)) (hs : { u | GenerateOpen s u } = s) :
    TopologicalSpace α where
  IsOpen u := u ∈ s
  isOpen_univ := hs ▸ TopologicalSpace.GenerateOpen.univ
  isOpen_inter := hs ▸ TopologicalSpace.GenerateOpen.inter
  isOpen_sUnion := hs ▸ TopologicalSpace.GenerateOpen.sUnion

Topology generated by a collection of sets

Informal description

Given a collection of sets $s$ in a type $\alpha$ such that $s$ is exactly the collection of open sets generated by $s$ (i.e., $\{u \mid \text{GenerateOpen } s \ u\} = s$), the function `TopologicalSpace.mkOfClosure` constructs a topology on $\alpha$ where a set is open if and only if it belongs to $s$. This topology is the least topology containing $s$.

TopologicalSpace.mkOfClosure_sets theorem

{s : Set (Set α)} {hs : {u | GenerateOpen s u} = s} : TopologicalSpace.mkOfClosure s hs = generateFrom s

Full source

theorem mkOfClosure_sets {s : Set (Set α)} {hs : { u | GenerateOpen s u } = s} :
    TopologicalSpace.mkOfClosure s hs = generateFrom s :=
  TopologicalSpace.ext hs.symm

Equality of Generated Topology and Closure-Constructed Topology

Informal description

For any collection of sets $s$ in a type $\alpha$ such that $s$ is exactly the collection of open sets generated by $s$ (i.e., $\{u \mid \text{GenerateOpen } s \ u\} = s$), the topology constructed by `TopologicalSpace.mkOfClosure` on $s$ with this condition is equal to the topology generated from $s$.

TopologicalSpace.gc_generateFrom theorem

 (α) :
  GaloisConnection (fun t : TopologicalSpace α => OrderDual.toDual {s | IsOpen[t] s}) (generateFrom ∘ OrderDual.ofDual)

Full source

theorem gc_generateFrom (α) :
    GaloisConnection (fun t : TopologicalSpace α => OrderDual.toDual { s | IsOpen[t] s })
      (generateFromgenerateFrom ∘ OrderDual.ofDual) := fun _ _ =>
  le_generateFrom_iff_subset_isOpen.symm

Galois Connection Between Topologies and Open Sets via Generation

Informal description

For any type $\alpha$, there is a Galois connection between the collection of all topologies on $\alpha$ (ordered by reverse inclusion) and the collection of all sets of subsets of $\alpha$ (also ordered by reverse inclusion). Specifically, the connection is given by the functions: - $F(t) = \{s \mid \text{IsOpen}[t]\ s\}^\mathrm{op}$, which maps a topology $t$ to the opposite of its collection of open sets, and - $G(g) = \text{generateFrom}(g^\mathrm{op})$, which generates a topology from the opposite of a collection of subsets $g$. Here, $^\mathrm{op}$ denotes the order dual (reverse inclusion order).

TopologicalSpace.gciGenerateFrom definition

 (α : Type*) :
  GaloisCoinsertion (fun t : TopologicalSpace α => OrderDual.toDual {s | IsOpen[t] s}) (generateFrom ∘ OrderDual.ofDual)

Full source

/-- The Galois coinsertion between `TopologicalSpace α` and `(Set (Set α))ᵒᵈ` whose lower part sends
  a topology to its collection of open subsets, and whose upper part sends a collection of subsets
  of `α` to the topology they generate. -/
def gciGenerateFrom (α : Type*) :
    GaloisCoinsertion (fun t : TopologicalSpace α => OrderDual.toDual { s | IsOpen[t] s })
      (generateFromgenerateFrom ∘ OrderDual.ofDual) where
  gc := gc_generateFrom α
  u_l_le _ s hs := TopologicalSpace.GenerateOpen.basic s hs
  choice g hg := TopologicalSpace.mkOfClosure g
    (Subset.antisymm hg <| le_generateFrom_iff_subset_isOpen.1 <| le_rfl)
  choice_eq _ _ := mkOfClosure_sets

Galois Coinsertion Between Topologies and Open Sets via Generation

Informal description

For any type $\alpha$, there is a Galois coinsertion between the collection of all topologies on $\alpha$ (ordered by reverse inclusion) and the collection of all sets of subsets of $\alpha$ (also ordered by reverse inclusion). Specifically, the coinsertion is given by the functions: - $F(t) = \{s \mid \text{IsOpen}[t]\ s\}^\mathrm{op}$, which maps a topology $t$ to the opposite of its collection of open sets, and - $G(g) = \text{generateFrom}(g^\mathrm{op})$, which generates a topology from the opposite of a collection of subsets $g$. Here, $^\mathrm{op}$ denotes the order dual (reverse inclusion order). The coinsertion ensures that $F$ and $G$ form a Galois connection where $G$ is injective, and provides a way to construct a topology from a collection of sets that generates it.

TopologicalSpace.instCompleteLattice instance

: CompleteLattice (TopologicalSpace α)

Full source

/-- Topologies on `α` form a complete lattice, with `⊥` the discrete topology
  and `⊤` the indiscrete topology. The infimum of a collection of topologies
  is the topology generated by all their open sets, while the supremum is the
  topology whose open sets are those sets open in every member of the collection. -/
instance : CompleteLattice (TopologicalSpace α) := (gciGenerateFrom α).liftCompleteLattice

Complete Lattice Structure on Topologies

Informal description

The collection of all topologies on a fixed type $\alpha$ forms a complete lattice under the reverse inclusion order, where: - The infimum (meet) of a collection of topologies is the topology generated by all their open sets. - The supremum (join) is the topology whose open sets are precisely those sets that are open in every member of the collection. - The bottom element $\bot$ is the discrete topology (where every set is open). - The top element $\top$ is the indiscrete topology (where only $\emptyset$ and $\alpha$ are open).

TopologicalSpace.generateFrom_anti theorem

{α} {g₁ g₂ : Set (Set α)} (h : g₁ ⊆ g₂) : generateFrom g₂ ≤ generateFrom g₁

Full source

@[mono, gcongr]
theorem generateFrom_anti {α} {g₁ g₂ : Set (Set α)} (h : g₁ ⊆ g₂) :
    generateFrom g₂ ≤ generateFrom g₁ :=
  (gc_generateFrom _).monotone_u h

Antitonicity of Topology Generation: $g_1 \subseteq g_2$ implies $\text{generateFrom}\ g_2 \leq \text{generateFrom}\ g_1$

Informal description

For any type $\alpha$ and any two collections of subsets $g_1$ and $g_2$ of $\alpha$, if $g_1 \subseteq g_2$, then the topology generated by $g_2$ is finer than the topology generated by $g_1$ (i.e., $\text{generateFrom}\ g_2 \leq \text{generateFrom}\ g_1$).

TopologicalSpace.generateFrom_setOf_isOpen theorem

(t : TopologicalSpace α) : generateFrom {s | IsOpen[t] s} = t

Full source

theorem generateFrom_setOf_isOpen (t : TopologicalSpace α) :
    generateFrom { s | IsOpen[t] s } = t :=
  (gciGenerateFrom α).u_l_eq t

Topology Generation from Open Sets Yields Original Topology

Informal description

For any topological space $t$ on a type $\alpha$, the topology generated by the collection of all open sets in $t$ is equal to $t$ itself. In other words, $\text{generateFrom}\ \{s \mid \text{IsOpen}[t]\ s\} = t$.

TopologicalSpace.leftInverse_generateFrom theorem

: LeftInverse generateFrom fun t : TopologicalSpace α => {s | IsOpen[t] s}

Full source

theorem leftInverse_generateFrom :
    LeftInverse generateFrom fun t : TopologicalSpace α => { s | IsOpen[t] s } :=
  (gciGenerateFrom α).u_l_leftInverse

Recovery of Topology from its Open Sets via Generation

Informal description

The function `generateFrom` is a left inverse to the function that maps a topology `t` on a type `α` to the collection of open sets in `t`. That is, for any topology `t` on `α`, generating a topology from the open sets of `t` returns `t` itself. In other words, if we take the open sets of a topology and then generate a new topology from those sets, we recover the original topology.

TopologicalSpace.generateFrom_surjective theorem

: Surjective (generateFrom : Set (Set α) → TopologicalSpace α)

Full source

theorem generateFrom_surjective : Surjective (generateFrom : Set (Set α) → TopologicalSpace α) :=
  (gciGenerateFrom α).u_surjective

Surjectivity of Topology Generation from Subsets

Informal description

The function `generateFrom` that maps a collection of subsets of $\alpha$ to the topology generated by that collection is surjective. That is, for every topology $t$ on $\alpha$, there exists a collection of subsets $g$ such that the topology generated by $g$ is equal to $t$.

TopologicalSpace.setOf_isOpen_injective theorem

: Injective fun t : TopologicalSpace α => {s | IsOpen[t] s}

Full source

theorem setOf_isOpen_injective : Injective fun t : TopologicalSpace α => { s | IsOpen[t] s } :=
  (gciGenerateFrom α).l_injective

Injectivity of Topology to Open Sets Mapping

Informal description

The function that maps a topology $t$ on a type $\alpha$ to its collection of open sets $\{s \mid \text{IsOpen}[t]\ s\}$ is injective. In other words, if two topologies on $\alpha$ have the same open sets, then they are equal.

IsOpen.mono theorem

(hs : IsOpen[t₂] s) (h : t₁ ≤ t₂) : IsOpen[t₁] s

Full source

theorem IsOpen.mono (hs : IsOpen[t₂] s) (h : t₁ ≤ t₂) : IsOpen[t₁] s := h s hs

Monotonicity of Open Sets with Respect to Finer Topologies

Informal description

Let $t_1$ and $t_2$ be two topologies on a type $\alpha$ such that $t_1 \leq t_2$ (i.e., $t_1$ is finer than $t_2$). If a set $s$ is open in the topology $t_2$, then $s$ is also open in the topology $t_1$.

IsClosed.mono theorem

(hs : IsClosed[t₂] s) (h : t₁ ≤ t₂) : IsClosed[t₁] s

Full source

theorem IsClosed.mono (hs : IsClosed[t₂] s) (h : t₁ ≤ t₂) : IsClosed[t₁] s :=
  (@isOpen_compl_iff α s t₁).mp <| hs.isOpen_compl.mono h

Monotonicity of Closed Sets with Respect to Finer Topologies

Informal description

Let $t_1$ and $t_2$ be two topologies on a type $\alpha$ such that $t_1 \leq t_2$ (i.e., $t_1$ is finer than $t_2$). If a subset $s \subseteq \alpha$ is closed in the topology $t_2$, then $s$ is also closed in the topology $t_1$.

closure.mono theorem

(h : t₁ ≤ t₂) : closure[t₁] s ⊆ closure[t₂] s

Full source

theorem closure.mono (h : t₁ ≤ t₂) : closure[t₁]closure[t₁] s ⊆ closure[t₂] s :=
  @closure_minimal _ t₁ s (@closure _ t₂ s) subset_closure (IsClosed.mono isClosed_closure h)

Monotonicity of Closure with Respect to Finer Topologies

Informal description

For any two topologies $t_1$ and $t_2$ on a type $\alpha$ such that $t_1 \leq t_2$ (i.e., $t_1$ is finer than $t_2$), the closure of any subset $s \subseteq \alpha$ under $t_1$ is contained in its closure under $t_2$. In other words, $\text{closure}_{t_1}(s) \subseteq \text{closure}_{t_2}(s)$.

isOpen_implies_isOpen_iff theorem

: (∀ s, IsOpen[t₁] s → IsOpen[t₂] s) ↔ t₂ ≤ t₁

Full source

theorem isOpen_implies_isOpen_iff : (∀ s, IsOpen[t₁] s → IsOpen[t₂] s) ↔ t₂ ≤ t₁ :=
  Iff.rfl

Characterization of Topological Fineness via Open Sets

Informal description

For two topological spaces $t₁$ and $t₂$ on a type $\alpha$, the following are equivalent: 1. Every set that is open in $t₁$ is also open in $t₂$. 2. The topology $t₂$ is coarser than $t₁$ (i.e., $t₂ \leq t₁$ in the partial order of topologies).

TopologicalSpace.isOpen_top_iff theorem

{α} (U : Set α) : IsOpen[⊤] U ↔ U = ∅ ∨ U = univ

Full source

/-- The only open sets in the indiscrete topology are the empty set and the whole space. -/
theorem TopologicalSpace.isOpen_top_iff {α} (U : Set α) : IsOpen[⊤]IsOpen[⊤] U ↔ U = ∅ ∨ U = univ :=
  ⟨fun h => by
    induction h with
    | basic _ h => exact False.elim h
    | univ => exact .inr rfl
    | inter _ _ _ _ h₁ h₂ =>
      rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
    | sUnion _ _ ih => exact sUnion_mem_empty_univ ih, by
      rintro (rfl | rfl)
      exacts [@isOpen_empty _ ⊤, @isOpen_univ _ ⊤]⟩

Characterization of Open Sets in the Indiscrete Topology: $U$ is open iff $U = \emptyset$ or $U = \text{univ}$

Informal description

For any set $U$ in a topological space $\alpha$ with the indiscrete topology $\top$, $U$ is open if and only if $U$ is either the empty set or the entire space $\alpha$. In other words, $\text{IsOpen}_{\top}(U) \leftrightarrow (U = \emptyset \lor U = \text{univ})$.

DiscreteTopology structure

(α : Type*) [t : TopologicalSpace α]

Full source

/-- A topological space is discrete if every set is open, that is,
  its topology equals the discrete topology `⊥`. -/
class DiscreteTopology (α : Type*) [t : TopologicalSpace α] : Prop where
  /-- The `TopologicalSpace` structure on a type with discrete topology is equal to `⊥`. -/
  eq_bot : t = ⊥

Discrete Topological Space

Informal description

A topological space $(α, t)$ is called discrete if every subset of $α$ is open, i.e., the topology $t$ is the finest possible topology (the discrete topology).

discreteTopology_bot theorem

(α : Type*) : @DiscreteTopology α ⊥

Full source

theorem discreteTopology_bot (α : Type*) : @DiscreteTopology α ⊥ :=
  @DiscreteTopology.mk α ⊥ rfl

Discrete Topology is the Bottom Element

Informal description

For any type $\alpha$, the bottom element $\bot$ in the lattice of topologies on $\alpha$ (i.e., the discrete topology) makes $\alpha$ a discrete topological space.

isOpen_discrete theorem

(s : Set α) : IsOpen s

Full source

@[simp]
theorem isOpen_discrete (s : Set α) : IsOpen s := (@DiscreteTopology.eq_bot α _).symm ▸ trivial

All Subsets are Open in Discrete Topology

Informal description

For any subset $s$ of a type $\alpha$ equipped with the discrete topology, $s$ is an open set.

isClosed_discrete theorem

(s : Set α) : IsClosed s

Full source

@[simp] theorem isClosed_discrete (s : Set α) : IsClosed s := ⟨isOpen_discrete _⟩

All Subsets are Closed in Discrete Topology

Informal description

For any subset $s$ of a type $\alpha$ equipped with the discrete topology, $s$ is a closed set.

closure_discrete theorem

(s : Set α) : closure s = s

Full source

theorem closure_discrete (s : Set α) : closure s = s := (isClosed_discrete _).closure_eq

Closure in Discrete Topology Equals Original Set

Informal description

For any subset $s$ of a type $\alpha$ equipped with the discrete topology, the closure of $s$ is equal to $s$ itself.

dense_discrete theorem

{s : Set α} : Dense s ↔ s = univ

Full source

@[simp] theorem dense_discrete {s : Set α} : DenseDense s ↔ s = univ := by simp [dense_iff_closure_eq]

Density in Discrete Space: $s$ is dense iff $s = \text{univ}$

Informal description

A subset $s$ of a discrete topological space $\alpha$ is dense if and only if $s$ is equal to the universal set $\text{univ}$ (i.e., $s$ contains all elements of $\alpha$).

denseRange_discrete theorem

{ι : Type*} {f : ι → α} : DenseRange f ↔ Surjective f

Full source

@[simp]
theorem denseRange_discrete {ι : Type*} {f : ι → α} : DenseRangeDenseRange f ↔ Surjective f := by
  rw [DenseRange, dense_discrete, range_eq_univ]

Density of Range in Discrete Space iff Function is Surjective

Informal description

For any function $f : \iota \to \alpha$ from a type $\iota$ to a discrete topological space $\alpha$, the range of $f$ is dense if and only if $f$ is surjective. In other words, $\text{DenseRange}(f) \leftrightarrow \text{Surjective}(f)$.

continuous_of_discreteTopology theorem

[TopologicalSpace β] {f : α → β} : Continuous f

Full source

@[nontriviality, continuity, fun_prop]
theorem continuous_of_discreteTopology [TopologicalSpace β] {f : α → β} : Continuous f :=
  continuous_def.2 fun _ _ => isOpen_discrete _

Continuity of Functions from Discrete Topological Spaces

Informal description

Let $\alpha$ be a type equipped with the discrete topology and $\beta$ be any topological space. Then any function $f : \alpha \to \beta$ is continuous.

continuous_discrete_rng theorem

 {α} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] {f : α → β} :
  Continuous f ↔ ∀ b : β, IsOpen (f ⁻¹' { b })

Full source

/-- A function to a discrete topological space is continuous if and only if the preimage of every
singleton is open. -/
theorem continuous_discrete_rng {α} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β]
    {f : α → β} : ContinuousContinuous f ↔ ∀ b : β, IsOpen (f ⁻¹' {b}) :=
  ⟨fun h _ => (isOpen_discrete _).preimage h, fun h => ⟨fun s _ => by
    rw [← biUnion_of_singleton s, preimage_iUnion₂]
    exact isOpen_biUnion fun _ _ => h _⟩⟩

Characterization of Continuity for Functions to Discrete Spaces

Informal description

Let $X$ and $Y$ be topological spaces where $Y$ has the discrete topology. A function $f \colon X \to Y$ is continuous if and only if for every $y \in Y$, the preimage $f^{-1}(\{y\})$ is an open set in $X$.

nhds_discrete theorem

(α : Type*) [TopologicalSpace α] [DiscreteTopology α] : @nhds α _ = pure

Full source

@[simp]
theorem nhds_discrete (α : Type*) [TopologicalSpace α] [DiscreteTopology α] : @nhds α _ = pure :=
  le_antisymm (fun _ s hs => (isOpen_discrete s).mem_nhds hs) pure_le_nhds

Neighborhood Filter in Discrete Topology Equals Principal Ultrafilter

Informal description

For any topological space $\alpha$ equipped with the discrete topology, the neighborhood filter $\mathcal{N}(x)$ at any point $x \in \alpha$ is equal to the principal ultrafilter $\{x\}$.

mem_nhds_discrete theorem

{x : α} {s : Set α} : s ∈ 𝓝 x ↔ x ∈ s

Full source

theorem mem_nhds_discrete {x : α} {s : Set α} :
    s ∈ 𝓝 xs ∈ 𝓝 x ↔ x ∈ s := by rw [nhds_discrete, mem_pure]

Neighborhood Membership in Discrete Topology: $s \in \mathcal{N}(x) \leftrightarrow x \in s$

Informal description

Let $\alpha$ be a topological space with the discrete topology. For any point $x \in \alpha$ and any subset $s \subseteq \alpha$, the neighborhood filter $\mathcal{N}(x)$ contains $s$ if and only if $x$ belongs to $s$.

le_of_nhds_le_nhds theorem

(h : ∀ x, @nhds α t₁ x ≤ @nhds α t₂ x) : t₁ ≤ t₂

Full source

theorem le_of_nhds_le_nhds (h : ∀ x, @nhds α t₁ x ≤ @nhds α t₂ x) : t₁ ≤ t₂ := fun s => by
  rw [@isOpen_iff_mem_nhds _ t₁, @isOpen_iff_mem_nhds _ t₂]
  exact fun hs a ha => h _ (hs _ ha)

Comparison of Topologies via Neighborhood Filters

Informal description

Let $t_1$ and $t_2$ be two topologies on a type $\alpha$. If for every point $x \in \alpha$, the neighborhood filter $\mathcal{N}_{t_1}(x)$ is finer than $\mathcal{N}_{t_2}(x)$ (i.e., $\mathcal{N}_{t_1}(x) \leq \mathcal{N}_{t_2}(x)$), then $t_1$ is finer than $t_2$ (i.e., $t_1 \leq t_2$).

forall_open_iff_discrete theorem

{X : Type*} [TopologicalSpace X] : (∀ s : Set X, IsOpen s) ↔ DiscreteTopology X

Full source

theorem forall_open_iff_discrete {X : Type*} [TopologicalSpace X] :
    (∀ s : Set X, IsOpen s) ↔ DiscreteTopology X :=
  ⟨fun h => ⟨eq_bot_of_singletons_open fun _ => h _⟩, @isOpen_discrete _ _⟩

Discrete Topology Characterization via Open Sets

Informal description

For a topological space $(X, \tau)$, every subset of $X$ is open if and only if the topology $\tau$ is discrete.

discreteTopology_iff_forall_isClosed theorem

[TopologicalSpace α] : DiscreteTopology α ↔ ∀ s : Set α, IsClosed s

Full source

theorem discreteTopology_iff_forall_isClosed [TopologicalSpace α] :
    DiscreteTopologyDiscreteTopology α ↔ ∀ s : Set α, IsClosed s :=
  forall_open_iff_discrete.symm.trans <| compl_surjective.forall.trans <| forall_congr' fun _ ↦
    isOpen_compl_iff

Discrete Topology Characterization via Closed Sets

Informal description

A topological space $(α, \tau)$ has the discrete topology if and only if every subset of $α$ is closed.

singletons_open_iff_discrete theorem

{X : Type*} [TopologicalSpace X] : (∀ a : X, IsOpen ({ a } : Set X)) ↔ DiscreteTopology X

Full source

theorem singletons_open_iff_discrete {X : Type*} [TopologicalSpace X] :
    (∀ a : X, IsOpen ({a} : Set X)) ↔ DiscreteTopology X :=
  ⟨fun h => ⟨eq_bot_of_singletons_open h⟩, fun a _ => @isOpen_discrete _ _ a _⟩

Discrete Topology Characterization via Open Singletons

Informal description

For a topological space $(X, \tau)$, every singleton set $\{a\}$ is open in $\tau$ if and only if $X$ has the discrete topology.

DiscreteTopology.of_finite_of_isClosed_singleton theorem

[TopologicalSpace α] [Finite α] (h : ∀ a : α, IsClosed { a }) : DiscreteTopology α

Full source

theorem DiscreteTopology.of_finite_of_isClosed_singleton [TopologicalSpace α] [Finite α]
    (h : ∀ a : α, IsClosed {a}) : DiscreteTopology α :=
  discreteTopology_iff_forall_isClosed.mpr fun s ↦
    s.iUnion_of_singleton_coe ▸ isClosed_iUnion_of_finite fun _ ↦ h _

Finite Space with Closed Singletons is Discrete

Informal description

Let $\alpha$ be a finite topological space. If every singleton subset $\{a\}$ of $\alpha$ is closed, then $\alpha$ has the discrete topology.

discreteTopology_iff_singleton_mem_nhds theorem

[TopologicalSpace α] : DiscreteTopology α ↔ ∀ x : α, { x } ∈ 𝓝 x

Full source

theorem discreteTopology_iff_singleton_mem_nhds [TopologicalSpace α] :
    DiscreteTopologyDiscreteTopology α ↔ ∀ x : α, {x} ∈ 𝓝 x := by
  simp only [← singletons_open_iff_discrete, isOpen_iff_mem_nhds, mem_singleton_iff, forall_eq]

Discrete Topology Characterization via Singleton Neighborhoods

Informal description

A topological space $(X, \tau)$ is discrete if and only if for every point $x \in X$, the singleton set $\{x\}$ is a neighborhood of $x$ (i.e., $\{x\} \in \mathcal{N}(x)$, where $\mathcal{N}(x)$ denotes the neighborhood filter at $x$).

discreteTopology_iff_nhds theorem

[TopologicalSpace α] : DiscreteTopology α ↔ ∀ x : α, 𝓝 x = pure x

Full source

/-- This lemma characterizes discrete topological spaces as those whose singletons are
neighbourhoods. -/
theorem discreteTopology_iff_nhds [TopologicalSpace α] :
    DiscreteTopologyDiscreteTopology α ↔ ∀ x : α, 𝓝 x = pure x := by
  simp [discreteTopology_iff_singleton_mem_nhds, le_pure_iff]
  apply forall_congr' (fun x ↦ ?_)
  simp [le_antisymm_iff, pure_le_nhds x]

Discrete Topology Characterization via Neighborhood Filters

Informal description

A topological space $(X, \tau)$ is discrete if and only if for every point $x \in X$, the neighborhood filter $\mathcal{N}(x)$ is equal to the principal ultrafilter $\{x\}$.

discreteTopology_iff_nhds_ne theorem

[TopologicalSpace α] : DiscreteTopology α ↔ ∀ x : α, 𝓝[≠] x = ⊥

Full source

theorem discreteTopology_iff_nhds_ne [TopologicalSpace α] :
    DiscreteTopologyDiscreteTopology α ↔ ∀ x : α, 𝓝[≠] x = ⊥ := by
  simp only [discreteTopology_iff_singleton_mem_nhds, nhdsWithin, inf_principal_eq_bot, compl_compl]

Discrete Topology Characterization via Punctured Neighborhoods

Informal description

A topological space $(X, \tau)$ is discrete if and only if for every point $x \in X$, the neighborhood filter of $x$ restricted to the punctured neighborhood (i.e., excluding $x$ itself) is the trivial filter $\bot$.

DiscreteTopology.of_continuous_injective theorem

 {β : Type*} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] {f : α → β} (hc : Continuous f)
  (hinj : Injective f) : DiscreteTopology α

Full source

/-- If the codomain of a continuous injective function has discrete topology,
then so does the domain.

See also `Embedding.discreteTopology` for an important special case. -/
theorem DiscreteTopology.of_continuous_injective
    {β : Type*} [TopologicalSpace α] [TopologicalSpace β] [DiscreteTopology β] {f : α → β}
    (hc : Continuous f) (hinj : Injective f) : DiscreteTopology α :=
  forall_open_iff_discrete.1 fun s ↦ hinj.preimage_image s ▸ (isOpen_discrete _).preimage hc

Discrete Topology Induced by Continuous Injective Map

Informal description

Let $\alpha$ and $\beta$ be topological spaces, with $\beta$ having the discrete topology. If $f : \alpha \to \beta$ is a continuous injective function, then $\alpha$ also has the discrete topology.

isOpen_induced_iff theorem

[t : TopologicalSpace β] {s : Set α} {f : α → β} : IsOpen[t.induced f] s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s

Full source

theorem isOpen_induced_iff [t : TopologicalSpace β] {s : Set α} {f : α → β} :
    IsOpen[t.induced f]IsOpen[t.induced f] s ↔ ∃ t, IsOpen t ∧ f ⁻¹' t = s :=
  Iff.rfl

Characterization of Open Sets in Induced Topology via Preimage Condition

Informal description

Let $t$ be a topology on a type $\beta$, $f : \alpha \to \beta$ a function, and $s \subseteq \alpha$ a subset. Then $s$ is open in the induced topology on $\alpha$ (via $f$) if and only if there exists an open set $t$ in $\beta$ such that its preimage $f^{-1}(t)$ equals $s$.

isClosed_induced_iff theorem

 [t : TopologicalSpace β] {s : Set α} {f : α → β} : IsClosed[t.induced f] s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s

Full source

theorem isClosed_induced_iff [t : TopologicalSpace β] {s : Set α} {f : α → β} :
    IsClosed[t.induced f]IsClosed[t.induced f] s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s := by
  letI := t.induced f
  simp only [← isOpen_compl_iff, isOpen_induced_iff]
  exact compl_surjective.exists.trans (by simp only [preimage_compl, compl_inj_iff])

Characterization of Closed Sets in Induced Topology via Preimage Condition

Informal description

Let $\beta$ be a topological space with topology $t$, $f : \alpha \to \beta$ a function, and $s \subseteq \alpha$ a subset. Then $s$ is closed in the topology induced on $\alpha$ by $f$ if and only if there exists a closed set $t$ in $\beta$ such that the preimage $f^{-1}(t)$ equals $s$.

isOpen_coinduced theorem

{t : TopologicalSpace α} {s : Set β} {f : α → β} : IsOpen[t.coinduced f] s ↔ IsOpen (f ⁻¹' s)

Full source

theorem isOpen_coinduced {t : TopologicalSpace α} {s : Set β} {f : α → β} :
    IsOpen[t.coinduced f]IsOpen[t.coinduced f] s ↔ IsOpen (f ⁻¹' s) :=
  Iff.rfl

Openness in Coinduced Topology via Preimage Condition

Informal description

Let $t$ be a topology on a type $\alpha$, $f : \alpha \to \beta$ a function, and $s \subseteq \beta$ a subset. Then $s$ is open in the coinduced topology on $\beta$ (via $f$) if and only if its preimage $f^{-1}(s)$ is open in the original topology $t$ on $\alpha$.

isClosed_coinduced theorem

{t : TopologicalSpace α} {s : Set β} {f : α → β} : IsClosed[t.coinduced f] s ↔ IsClosed (f ⁻¹' s)

Full source

theorem isClosed_coinduced {t : TopologicalSpace α} {s : Set β} {f : α → β} :
    IsClosed[t.coinduced f]IsClosed[t.coinduced f] s ↔ IsClosed (f ⁻¹' s) := by
  simp only [← isOpen_compl_iff, isOpen_coinduced (f := f), preimage_compl]

Closedness in Coinduced Topology via Preimage Condition

Informal description

Let $t$ be a topology on a type $\alpha$, $f : \alpha \to \beta$ a function, and $s \subseteq \beta$ a subset. Then $s$ is closed in the coinduced topology on $\beta$ (via $f$) if and only if its preimage $f^{-1}(s)$ is closed in the original topology $t$ on $\alpha$.

preimage_nhds_coinduced theorem

 [TopologicalSpace α] {π : α → β} {s : Set β} {a : α} (hs : s ∈ @nhds β (TopologicalSpace.coinduced π ‹_›) (π a)) :
  π ⁻¹' s ∈ 𝓝 a

Full source

theorem preimage_nhds_coinduced [TopologicalSpace α] {π : α → β} {s : Set β} {a : α}
    (hs : s ∈ @nhds β (TopologicalSpace.coinduced π ‹_›) (π a)) : π ⁻¹' sπ ⁻¹' s ∈ 𝓝 a := by
  letI := TopologicalSpace.coinduced π ‹_›
  rcases mem_nhds_iff.mp hs with ⟨V, hVs, V_op, mem_V⟩
  exact mem_nhds_iff.mpr ⟨π ⁻¹' V, Set.preimage_mono hVs, V_op, mem_V⟩

Preimage of Neighborhood in Coinduced Topology is Neighborhood

Informal description

Let $(X, \tau)$ be a topological space, $\pi : X \to Y$ a function, and $s \subseteq Y$ a subset. If $s$ is a neighborhood of $\pi(a)$ in the coinduced topology on $Y$ (via $\pi$), then the preimage $\pi^{-1}(s)$ is a neighborhood of $a$ in $X$.

Continuous.coinduced_le theorem

(h : Continuous[t, t'] f) : t.coinduced f ≤ t'

Full source

theorem Continuous.coinduced_le (h : Continuous[t, t'] f) : t.coinduced f ≤ t' :=
  (@continuous_def α β t t').1 h

Coinduced Topology is Coarser for Continuous Maps

Informal description

Let $f : (X, t) \to (Y, t')$ be a continuous function between topological spaces. Then the coinduced topology on $Y$ by $f$ is coarser than $t'$, i.e., $t.\text{coinduced}\, f \leq t'$.

coinduced_le_iff_le_induced theorem

 {f : α → β} {tα : TopologicalSpace α} {tβ : TopologicalSpace β} : tα.coinduced f ≤ tβ ↔ tα ≤ tβ.induced f

Full source

theorem coinduced_le_iff_le_induced {f : α → β} {tα : TopologicalSpace α}
    {tβ : TopologicalSpace β} : tα.coinduced f ≤ tβ ↔ tα ≤ tβ.induced f :=
  ⟨fun h _s ⟨_t, ht, hst⟩ => hst ▸ h _ ht, fun h s hs => h _ ⟨s, hs, rfl⟩⟩

Equivalence of Coinduced and Induced Topology Orderings

Informal description

For any function $f : \alpha \to \beta$ between topological spaces $(α, tα)$ and $(β, tβ)$, the coinduced topology $tα.\text{coinduced}\, f$ on $\beta$ is coarser than $tβ$ if and only if the topology $tα$ on $\alpha$ is finer than the induced topology $tβ.\text{induced}\, f$ on $\alpha$. In other words: $$ tα.\text{coinduced}\, f ≤ tβ \leftrightarrow tα ≤ tβ.\text{induced}\, f $$

Continuous.le_induced theorem

(h : Continuous[t, t'] f) : t ≤ t'.induced f

Full source

theorem Continuous.le_induced (h : Continuous[t, t'] f) : t ≤ t'.induced f :=
  coinduced_le_iff_le_induced.1 h.coinduced_le

Fineness of Topology Implies Fineness of Induced Topology for Continuous Maps

Informal description

Let $f : (X, t) \to (Y, t')$ be a continuous function between topological spaces. Then the topology $t$ on $X$ is finer than the topology induced by $f$ on $X$ from $t'$, i.e., $t \leq t'.\text{induced}\, f$.

gc_coinduced_induced theorem

(f : α → β) : GaloisConnection (TopologicalSpace.coinduced f) (TopologicalSpace.induced f)

Full source

theorem gc_coinduced_induced (f : α → β) :
    GaloisConnection (TopologicalSpace.coinduced f) (TopologicalSpace.induced f) := fun _ _ =>
  coinduced_le_iff_le_induced

Galois Connection Between Coinduced and Induced Topologies

Informal description

For any function $f \colon \alpha \to \beta$, the pair of functions $(T_{\text{coinduced}}(f), T_{\text{induced}}(f))$ forms a Galois connection between the lattice of topologies on $\alpha$ (ordered by reverse inclusion) and the lattice of topologies on $\beta$ (ordered by reverse inclusion). Here: - $T_{\text{coinduced}}(f)$ maps a topology on $\alpha$ to the coinduced topology on $\beta$, - $T_{\text{induced}}(f)$ maps a topology on $\beta$ to the induced topology on $\alpha$. This means that for any topology $t_\alpha$ on $\alpha$ and $t_\beta$ on $\beta$, we have: $$ T_{\text{coinduced}}(f)(t_\alpha) \leq t_\beta \iff t_\alpha \leq T_{\text{induced}}(f)(t_\beta) $$

induced_mono theorem

(h : t₁ ≤ t₂) : t₁.induced g ≤ t₂.induced g

Full source

theorem induced_mono (h : t₁ ≤ t₂) : t₁.induced g ≤ t₂.induced g :=
  (gc_coinduced_induced g).monotone_u h

Monotonicity of Induced Topology with Respect to Fineness

Informal description

Let $t_1$ and $t_2$ be two topologies on a type $\alpha$ such that $t_1$ is finer than $t_2$ (i.e., $t_1 \leq t_2$). Then for any function $g \colon \alpha \to \beta$, the topology induced by $g$ from $t_1$ is finer than the topology induced by $g$ from $t_2$, i.e., $t_1.\text{induced}\, g \leq t_2.\text{induced}\, g$.

coinduced_mono theorem

(h : t₁ ≤ t₂) : t₁.coinduced f ≤ t₂.coinduced f

Full source

theorem coinduced_mono (h : t₁ ≤ t₂) : t₁.coinduced f ≤ t₂.coinduced f :=
  (gc_coinduced_induced f).monotone_l h

Monotonicity of Coinduced Topology with Respect to Fineness

Informal description

For any function $f \colon \alpha \to \beta$ and topologies $t_1, t_2$ on $\alpha$, if $t_1$ is finer than $t_2$ (i.e., $t_1 \leq t_2$), then the coinduced topology on $\beta$ from $t_1$ is finer than the coinduced topology from $t_2$ (i.e., $t_1.\text{coinduced}(f) \leq t_2.\text{coinduced}(f)$).

induced_top theorem

: (⊤ : TopologicalSpace α).induced g = ⊤

Full source

@[simp]
theorem induced_top : (⊤ : TopologicalSpace α).induced g = ⊤ :=
  (gc_coinduced_induced g).u_top

Induced Topology from Indiscrete is Indiscrete

Informal description

For any function $g \colon \alpha \to \beta$, the topology induced on $\alpha$ from the indiscrete topology on $\beta$ is the indiscrete topology on $\alpha$, i.e., $(\top : \text{TopologicalSpace } \beta).\text{induced } g = \top$.

induced_inf theorem

: (t₁ ⊓ t₂).induced g = t₁.induced g ⊓ t₂.induced g

Full source

@[simp]
theorem induced_inf : (t₁ ⊓ t₂).induced g = t₁.induced g ⊓ t₂.induced g :=
  (gc_coinduced_induced g).u_inf

Induced Topology Preserves Infima of Topologies

Informal description

For any two topologies $t_1$ and $t_2$ on a type $\alpha$ and any function $g \colon \alpha \to \beta$, the topology induced by $g$ from the infimum (coarsest common refinement) of $t_1$ and $t_2$ is equal to the infimum of the topologies induced by $g$ from $t_1$ and $t_2$ individually. In other words: $$ (t_1 \sqcap t_2).\text{induced}(g) = t_1.\text{induced}(g) \sqcap t_2.\text{induced}(g) $$

induced_iInf theorem

{ι : Sort w} {t : ι → TopologicalSpace α} : (⨅ i, t i).induced g = ⨅ i, (t i).induced g

Full source

@[simp]
theorem induced_iInf {ι : Sort w} {t : ι → TopologicalSpace α} :
    (⨅ i, t i).induced g = ⨅ i, (t i).induced g :=
  (gc_coinduced_induced g).u_iInf

Infimum of Induced Topologies Equals Induced Topology of Infimum

Informal description

For any indexed family of topologies $\{t_i\}_{i \in \iota}$ on a type $\alpha$, the induced topology on $\beta$ via a function $g \colon \alpha \to \beta$ from the infimum of the family $\bigsqcap_i t_i$ is equal to the infimum of the induced topologies $\bigsqcap_i (t_i.\text{induced}\, g)$. In symbols: $$ \left(\bigsqcap_{i} t_i\right).\text{induced}\, g = \bigsqcap_{i} (t_i.\text{induced}\, g) $$

induced_sInf theorem

{s : Set (TopologicalSpace α)} : TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.induced g '' s)

Full source

@[simp]
theorem induced_sInf {s : Set (TopologicalSpace α)} :
    TopologicalSpace.induced g (sInf s) = sInf (TopologicalSpace.inducedTopologicalSpace.induced g '' s) := by
  rw [sInf_eq_iInf', sInf_image', induced_iInf]

Induced Topology Preserves Infima of Sets of Topologies

Informal description

For any set $s$ of topologies on a type $\alpha$ and any function $g \colon \alpha \to \beta$, the topology induced by $g$ from the infimum of $s$ is equal to the infimum of the set of topologies induced by $g$ from each topology in $s$. In symbols: $$ \text{induced}\, g \left(\bigsqcap s\right) = \bigsqcap \left(\text{induced}\, g \right)'' s $$

coinduced_bot theorem

: (⊥ : TopologicalSpace α).coinduced f = ⊥

Full source

@[simp]
theorem coinduced_bot : (⊥ : TopologicalSpace α).coinduced f = ⊥ :=
  (gc_coinduced_induced f).l_bot

Coinduced Topology from Discrete is Discrete

Informal description

For any function $f \colon \alpha \to \beta$, the coinduced topology on $\beta$ from the discrete topology on $\alpha$ is the discrete topology on $\beta$. In other words, $(\bot : \text{TopologicalSpace } \alpha).\text{coinduced } f = \bot$.

coinduced_sup theorem

: (t₁ ⊔ t₂).coinduced f = t₁.coinduced f ⊔ t₂.coinduced f

Full source

@[simp]
theorem coinduced_sup : (t₁ ⊔ t₂).coinduced f = t₁.coinduced f ⊔ t₂.coinduced f :=
  (gc_coinduced_induced f).l_sup

Coinduced Topology Preserves Suprema

Informal description

For any function $f \colon \alpha \to \beta$ and any two topologies $t_1$ and $t_2$ on $\alpha$, the coinduced topology on $\beta$ from the supremum topology $t_1 \sqcup t_2$ on $\alpha$ is equal to the supremum of the coinduced topologies from $t_1$ and $t_2$ individually. That is: $$ (t_1 \sqcup t_2)_{\text{coinduced}}(f) = t_{1,\text{coinduced}}(f) \sqcup t_{2,\text{coinduced}}(f) $$

coinduced_iSup theorem

{ι : Sort w} {t : ι → TopologicalSpace α} : (⨆ i, t i).coinduced f = ⨆ i, (t i).coinduced f

Full source

@[simp]
theorem coinduced_iSup {ι : Sort w} {t : ι → TopologicalSpace α} :
    (⨆ i, t i).coinduced f = ⨆ i, (t i).coinduced f :=
  (gc_coinduced_induced f).l_iSup

Coinduced Topology Preserves Suprema

Informal description

For any family of topologies $\{t_i\}_{i \in \iota}$ on a type $\alpha$ and any function $f \colon \alpha \to \beta$, the coinduced topology on $\beta$ from the supremum topology $\bigsqcup_i t_i$ on $\alpha$ is equal to the supremum of the coinduced topologies from each $t_i$. That is: $$ \left(\bigsqcup_{i} t_i\right).\text{coinduced}\, f = \bigsqcup_{i} (t_i.\text{coinduced}\, f) $$

coinduced_sSup theorem

{s : Set (TopologicalSpace α)} : TopologicalSpace.coinduced f (sSup s) = sSup ((TopologicalSpace.coinduced f) '' s)

Full source

@[simp]
theorem coinduced_sSup {s : Set (TopologicalSpace α)} :
    TopologicalSpace.coinduced f (sSup s) = sSup ((TopologicalSpace.coinduced f) '' s) := by
  rw [sSup_eq_iSup', sSup_image', coinduced_iSup]

Coinduced Topology Preserves Suprema of Sets of Topologies

Informal description

For any set $s$ of topologies on a type $\alpha$ and any function $f \colon \alpha \to \beta$, the coinduced topology on $\beta$ from the supremum topology $\bigsqcup s$ on $\alpha$ is equal to the supremum of the coinduced topologies from each topology in $s$. That is: $$ \left(\bigsqcup s\right).\text{coinduced}\, f = \bigsqcup \left(\text{coinduced}\, f\right)'' s $$

induced_id theorem

[t : TopologicalSpace α] : t.induced id = t

Full source

theorem induced_id [t : TopologicalSpace α] : t.induced id = t :=
  TopologicalSpace.ext <|
    funext fun s => propext <| ⟨fun ⟨_, hs, h⟩ => h ▸ hs, fun hs => ⟨s, hs, rfl⟩⟩

Identity Function Preserves Induced Topology

Informal description

For any topological space $t$ on a type $\alpha$, the topology induced on $\alpha$ by the identity function $\mathrm{id} : \alpha \to \alpha$ is equal to $t$ itself, i.e., $t.\text{induced}\, \mathrm{id} = t$.

induced_compose theorem

{tγ : TopologicalSpace γ} {f : α → β} {g : β → γ} : (tγ.induced g).induced f = tγ.induced (g ∘ f)

Full source

theorem induced_compose {tγ : TopologicalSpace γ} {f : α → β} {g : β → γ} :
    (tγ.induced g).induced f = tγ.induced (g ∘ f) :=
  TopologicalSpace.ext <|
    funext fun _ => propext
      ⟨fun ⟨_, ⟨s, hs, h₂⟩, h₁⟩ => h₁ ▸ h₂ ▸ ⟨s, hs, rfl⟩,
        fun ⟨s, hs, h⟩ => ⟨preimage g s, ⟨s, hs, rfl⟩, h ▸ rfl⟩⟩

Composition Rule for Induced Topologies

Informal description

For any topological space $t_\gamma$ on $\gamma$ and functions $f : \alpha \to \beta$ and $g : \beta \to \gamma$, the topology induced on $\alpha$ by $g \circ f$ is equal to the topology induced on $\alpha$ by $f$ from the topology induced on $\beta$ by $g$ from $t_\gamma$. In other words, $(t_\gamma.\text{induced}\, g).\text{induced}\, f = t_\gamma.\text{induced}\, (g \circ f)$.

induced_const theorem

[t : TopologicalSpace α] {x : α} : (t.induced fun _ : β => x) = ⊤

Full source

theorem induced_const [t : TopologicalSpace α] {x : α} : (t.induced fun _ : β => x) = ⊤ :=
  le_antisymm le_top (@continuous_const β α ⊤ t x).le_induced

Induced Topology by Constant Function is Indiscrete

Informal description

For any topological space $t$ on a type $\alpha$ and any fixed element $x \in \alpha$, the topology induced on $\beta$ by the constant function $f : \beta \to \alpha$ defined by $f(y) = x$ for all $y \in \beta$ is the indiscrete topology $\top$ on $\beta$.

coinduced_id theorem

[t : TopologicalSpace α] : t.coinduced id = t

Full source

theorem coinduced_id [t : TopologicalSpace α] : t.coinduced id = t :=
  TopologicalSpace.ext rfl

Coinduced Topology by Identity Map Preserves Original Topology

Informal description

For any topological space $t$ on a type $\alpha$, the coinduced topology on $\alpha$ by the identity map $\text{id} : \alpha \to \alpha$ is equal to $t$ itself, i.e., $t_{\text{coinduced}}(\text{id}) = t$.

coinduced_compose theorem

[tα : TopologicalSpace α] {f : α → β} {g : β → γ} : (tα.coinduced f).coinduced g = tα.coinduced (g ∘ f)

Full source

theorem coinduced_compose [tα : TopologicalSpace α] {f : α → β} {g : β → γ} :
    (tα.coinduced f).coinduced g = tα.coinduced (g ∘ f) :=
  TopologicalSpace.ext rfl

Composition Rule for Coinduced Topologies: $(t_\alpha)_{g \circ f} = (t_\alpha)_f_g$

Informal description

Let $\alpha$, $\beta$, and $\gamma$ be types, and let $t_\alpha$ be a topology on $\alpha$. For any functions $f : \alpha \to \beta$ and $g : \beta \to \gamma$, the coinduced topology on $\gamma$ from the coinduced topology on $\beta$ via $g$ is equal to the coinduced topology on $\gamma$ via the composition $g \circ f$. In other words, $(t_\alpha)_{\text{coinduced}}(f)_{\text{coinduced}}(g) = (t_\alpha)_{\text{coinduced}}(g \circ f)$.

Equiv.induced_symm theorem

{α β : Type*} (e : α ≃ β) : TopologicalSpace.induced e.symm = TopologicalSpace.coinduced e

Full source

theorem Equiv.induced_symm {α β : Type*} (e : α ≃ β) :
    TopologicalSpace.induced e.symm = TopologicalSpace.coinduced e := by
  ext t U
  rw [isOpen_induced_iff, isOpen_coinduced]
  simp only [e.symm.preimage_eq_iff_eq_image, exists_eq_right, ← preimage_equiv_eq_image_symm]

Equality of Induced and Coinduced Topologies via Equivalence: $\text{induced}(e^{-1}) = \text{coinduced}(e)$

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the topology induced on $\alpha$ by the inverse equivalence $e^{-1}$ is equal to the topology coinduced on $\alpha$ by $e$. That is, $\text{induced}(e^{-1}) = \text{coinduced}(e)$.

Equiv.coinduced_symm theorem

{α β : Type*} (e : α ≃ β) : TopologicalSpace.coinduced e.symm = TopologicalSpace.induced e

Full source

theorem Equiv.coinduced_symm {α β : Type*} (e : α ≃ β) :
    TopologicalSpace.coinduced e.symm = TopologicalSpace.induced e :=
  e.symm.induced_symm.symm

Equality of Coinduced and Induced Topologies via Inverse Equivalence: $\text{coinduced}(e^{-1}) = \text{induced}(e)$

Informal description

For any equivalence $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the topology coinduced on $\beta$ by the inverse equivalence $e^{-1}$ is equal to the topology induced on $\beta$ by $e$. That is, $\text{coinduced}(e^{-1}) = \text{induced}(e)$.

inhabitedTopologicalSpace instance

{α : Type u} : Inhabited (TopologicalSpace α)

Full source

instance inhabitedTopologicalSpace {α : Type u} : Inhabited (TopologicalSpace α) :=
  ⟨⊥⟩

Nonempty Collection of Topologies on a Type

Informal description

For any type $\alpha$, the collection of all possible topologies on $\alpha$ is nonempty.

Subsingleton.uniqueTopologicalSpace instance

[Subsingleton α] : Unique (TopologicalSpace α)

Full source

instance (priority := 100) Subsingleton.uniqueTopologicalSpace [Subsingleton α] :
    Unique (TopologicalSpace α) where
  default := ⊥
  uniq t :=
    eq_bot_of_singletons_open fun x =>
      Subsingleton.set_cases (@isOpen_empty _ t) (@isOpen_univ _ t) ({x} : Set α)

Unique Topology on Subsingleton Types

Informal description

For any type $\alpha$ that is a subsingleton (i.e., has at most one element), there is a unique topology on $\alpha$.

Subsingleton.discreteTopology instance

[t : TopologicalSpace α] [Subsingleton α] : DiscreteTopology α

Full source

instance (priority := 100) Subsingleton.discreteTopology [t : TopologicalSpace α] [Subsingleton α] :
    DiscreteTopology α :=
  ⟨Unique.eq_default t⟩

Subsingleton Topological Spaces are Discrete

Informal description

For any topological space $(α, t)$ where $α$ is a subsingleton (i.e., has at most one element), the topology $t$ is discrete (every subset of $α$ is open).

instTopologicalSpaceEmpty instance

: TopologicalSpace Empty

Full source

instance : TopologicalSpace Empty := ⊥

Topological Space Structure on the Empty Type

Informal description

The empty type $\text{Empty}$ is equipped with the canonical topological space structure.

instDiscreteTopologyEmpty instance

: DiscreteTopology Empty

Full source

instance : DiscreteTopology Empty := ⟨rfl⟩

Discrete Topology on the Empty Type

Informal description

The empty type $\text{Empty}$ is a discrete topological space, meaning every subset of $\text{Empty}$ is open.

instTopologicalSpacePEmpty instance

: TopologicalSpace PEmpty

Full source

instance : TopologicalSpace PEmpty := ⊥

Trivial Topology on the Empty Type

Informal description

The empty type `PEmpty` is equipped with the trivial topological space structure where the only open sets are the empty set and `PEmpty` itself.

instDiscreteTopologyPEmpty instance

: DiscreteTopology PEmpty

Full source

instance : DiscreteTopology PEmpty := ⟨rfl⟩

Discrete Topology on the Empty Type

Informal description

The empty type `PEmpty` is equipped with the discrete topology, where every subset is open.

instTopologicalSpacePUnit instance

: TopologicalSpace PUnit

Full source

instance : TopologicalSpace PUnit := ⊥

The Topological Space Structure on the Unit Type

Informal description

The type `PUnit` (the terminal object in the category of types) is equipped with a canonical topological space structure.

instDiscreteTopologyPUnit instance

: DiscreteTopology PUnit

Full source

instance : DiscreteTopology PUnit := ⟨rfl⟩

Discrete Topology on the Unit Type

Informal description

The unit type `PUnit` is equipped with the discrete topology, where every subset is open.

instTopologicalSpaceBool instance

: TopologicalSpace Bool

Full source

instance : TopologicalSpace Bool := ⊥

Topological Space Structure on Booleans

Informal description

The boolean type `Bool` is equipped with a canonical topological space structure.

instDiscreteTopologyBool instance

: DiscreteTopology Bool

Full source

instance : DiscreteTopology Bool := ⟨rfl⟩

Discrete Topology on Booleans

Informal description

The boolean type `Bool` is equipped with the discrete topology, where every subset is open.

instTopologicalSpaceNat instance

: TopologicalSpace ℕ

Full source

instance : TopologicalSpace ℕ := ⊥

The Topological Space Structure on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ are equipped with a canonical topological space structure.

instDiscreteTopologyNat instance

: DiscreteTopology ℕ

Full source

instance : DiscreteTopology ℕ := ⟨rfl⟩

Discrete Topology on Natural Numbers

Informal description

The natural numbers $\mathbb{N}$ are equipped with the discrete topology, where every subset is open.

instTopologicalSpaceInt instance

: TopologicalSpace ℤ

Full source

instance : TopologicalSpace ℤ := ⊥

The Topological Space Structure on Integers

Informal description

The integers $\mathbb{Z}$ are equipped with a canonical topological space structure.

instDiscreteTopologyInt instance

: DiscreteTopology ℤ

Full source

instance : DiscreteTopology ℤ := ⟨rfl⟩

Discrete Topology on the Integers

Informal description

The integers $\mathbb{Z}$ form a discrete topological space, where every subset of $\mathbb{Z}$ is open.

instTopologicalSpaceFin instance

{n} : TopologicalSpace (Fin n)

Full source

instance {n} : TopologicalSpace (Fin n) := ⊥

The Topological Space Structure on Finite Types

Informal description

For any natural number $n$, the finite type $\mathrm{Fin}(n)$ is equipped with a canonical topological space structure.

instDiscreteTopologyFin instance

{n} : DiscreteTopology (Fin n)

Full source

instance {n} : DiscreteTopology (Fin n) := ⟨rfl⟩

Discrete Topology on Finite Types

Informal description

For any natural number $n$, the finite type $\mathrm{Fin}(n)$ is equipped with the discrete topology, where every subset is open.

sierpinskiSpace instance

: TopologicalSpace Prop

Full source

instance sierpinskiSpace : TopologicalSpace Prop :=
  generateFrom {{True}}

The Sierpiński Topology on Propositions

Informal description

The type of propositions `Prop` is equipped with the Sierpiński topology, where the only open sets are the empty set, the entire space, and the set containing the true proposition.

continuous_empty_function theorem

[TopologicalSpace α] [TopologicalSpace β] [IsEmpty β] (f : α → β) : Continuous f

Full source

/-- See also `continuous_of_discreteTopology`, which works for `IsEmpty α`. -/
theorem continuous_empty_function [TopologicalSpace α] [TopologicalSpace β] [IsEmpty β]
    (f : α → β) : Continuous f :=
  letI := Function.isEmpty f
  continuous_of_discreteTopology

Continuity of Functions to Empty Topological Spaces

Informal description

Let $\alpha$ and $\beta$ be topological spaces with $\beta$ empty. Then any function $f \colon \alpha \to \beta$ is continuous.

le_generateFrom theorem

{t : TopologicalSpace α} {g : Set (Set α)} (h : ∀ s ∈ g, IsOpen s) : t ≤ generateFrom g

Full source

theorem le_generateFrom {t : TopologicalSpace α} {g : Set (Set α)} (h : ∀ s ∈ g, IsOpen s) :
    t ≤ generateFrom g :=
  le_generateFrom_iff_subset_isOpen.2 h

Fineness Criterion for Generated Topology: Open Sets Imply Finer Topology

Informal description

Let $t$ be a topological space on a type $\alpha$ and let $g$ be a collection of subsets of $\alpha$. If every set in $g$ is open in $t$, then $t$ is finer than the topology generated by $g$, i.e., $t \leq \text{generateFrom } g$.

induced_generateFrom_eq theorem

{α β} {b : Set (Set β)} {f : α → β} : (generateFrom b).induced f = generateFrom (preimage f '' b)

Full source

theorem induced_generateFrom_eq {α β} {b : Set (Set β)} {f : α → β} :
    (generateFrom b).induced f = generateFrom (preimagepreimage f '' b) :=
  le_antisymm (le_generateFrom <| forall_mem_image.2 fun s hs => ⟨s, GenerateOpen.basic _ hs, rfl⟩)
    (coinduced_le_iff_le_induced.1 <| le_generateFrom fun _s hs => .basic _ (mem_image_of_mem _ hs))

Equality of Induced Topology and Topology Generated by Preimages

Informal description

For any types $\alpha$ and $\beta$, collection of sets $b \subseteq \beta$, and function $f : \alpha \to \beta$, the topology on $\alpha$ induced by $f$ from the topology generated by $b$ is equal to the topology generated by the preimages of sets in $b$ under $f$. In symbols: $$ \text{induced}\, f (\text{generateFrom}\, b) = \text{generateFrom}\, (f^{-1} '' b) $$

le_induced_generateFrom theorem

 {α β} [t : TopologicalSpace α] {b : Set (Set β)} {f : α → β} (h : ∀ a : Set β, a ∈ b → IsOpen (f ⁻¹' a)) :
  t ≤ induced f (generateFrom b)

Full source

theorem le_induced_generateFrom {α β} [t : TopologicalSpace α] {b : Set (Set β)} {f : α → β}
    (h : ∀ a : Set β, a ∈ b → IsOpen (f ⁻¹' a)) : t ≤ induced f (generateFrom b) := by
  rw [induced_generateFrom_eq]
  apply le_generateFrom
  simp only [mem_image, and_imp, forall_apply_eq_imp_iff₂, exists_imp]
  exact h

Fineness Criterion for Induced Topology: Open Preimages Imply Finer Topology

Informal description

Let $\alpha$ and $\beta$ be types, with $t$ a topological space on $\alpha$. Given a collection of sets $b \subseteq \beta$ and a function $f : \alpha \to \beta$, if for every set $a \in b$ the preimage $f^{-1}(a)$ is open in $t$, then $t$ is finer than the topology on $\alpha$ induced by $f$ from the topology generated by $b$. In symbols: $$ t \leq \text{induced}\, f (\text{generateFrom}\, b) $$

generateFrom_insert_of_generateOpen theorem

{α : Type*} {s : Set (Set α)} {t : Set α} (ht : GenerateOpen s t) : generateFrom (insert t s) = generateFrom s

Full source

lemma generateFrom_insert_of_generateOpen {α : Type*} {s : Set (Set α)} {t : Set α}
    (ht : GenerateOpen s t) : generateFrom (insert t s) = generateFrom s := by
  refine le_antisymm (generateFrom_anti <| subset_insert t s) (le_generateFrom ?_)
  rintro t (rfl | h)
  · exact ht
  · exact isOpen_generateFrom_of_mem h

Equality of Generated Topologies When Adding a Generated Open Set

Informal description

Let $\alpha$ be a type, $s$ a collection of subsets of $\alpha$, and $t$ a subset of $\alpha$. If $t$ is open in the topology generated by $s$ (i.e., $\text{GenerateOpen}\, s\, t$ holds), then the topology generated by inserting $t$ into $s$ is equal to the topology generated by $s$ alone. In symbols: $$ \text{generateFrom}\, (\{t\} \cup s) = \text{generateFrom}\, s $$

generateFrom_insert_univ theorem

{α : Type*} {s : Set (Set α)} : generateFrom (insert univ s) = generateFrom s

Full source

@[simp]
lemma generateFrom_insert_univ {α : Type*} {s : Set (Set α)} :
    generateFrom (insert univ s) = generateFrom s :=
  generateFrom_insert_of_generateOpen .univ

Universal Set Redundancy in Topology Generation

Informal description

For any type $\alpha$ and any collection of subsets $s$ of $\alpha$, the topology generated by inserting the universal set $\text{univ}$ into $s$ is equal to the topology generated by $s$ alone. In symbols: $$ \text{generateFrom}\, (\{\text{univ}\} \cup s) = \text{generateFrom}\, s $$

generateFrom_insert_empty theorem

{α : Type*} {s : Set (Set α)} : generateFrom (insert ∅ s) = generateFrom s

Full source

@[simp]
lemma generateFrom_insert_empty {α : Type*} {s : Set (Set α)} :
    generateFrom (insert ∅ s) = generateFrom s := by
  rw [← sUnion_empty]
  exact generateFrom_insert_of_generateOpen (.sUnion ∅ (fun s_1 a ↦ False.elim a))

Topology Generation Unaffected by Adding Empty Set

Informal description

For any type $\alpha$ and any collection of subsets $s$ of $\alpha$, the topology generated by inserting the empty set into $s$ is equal to the topology generated by $s$ alone. In symbols: $$ \text{generateFrom}\, (\{\emptyset\} \cup s) = \text{generateFrom}\, s $$

nhdsAdjoint definition

(a : α) (f : Filter α) : TopologicalSpace α

Full source

/-- This construction is left adjoint to the operation sending a topology on `α`
  to its neighborhood filter at a fixed point `a : α`. -/
def nhdsAdjoint (a : α) (f : Filter α) : TopologicalSpace α where
  IsOpen s := a ∈ s → s ∈ f
  isOpen_univ _ := univ_mem
  isOpen_inter := fun _s _t hs ht ⟨has, hat⟩ => inter_mem (hs has) (ht hat)
  isOpen_sUnion := fun _k hk ⟨u, hu, hau⟩ => mem_of_superset (hk u hu hau) (subset_sUnion_of_mem hu)

Topology adjoint to a filter at a point

Informal description

Given a point $ a $ in a type $ \alpha $ and a filter $ f $ on $ \alpha $, the topology `nhdsAdjoint a f` on $ \alpha $ is defined as follows: a set $ s $ is open if whenever $ a \in s $, then $ s $ belongs to the filter $ f $. This construction satisfies the axioms of a topology: 1. The whole set $ \alpha $ is open. 2. The intersection of two open sets is open. 3. The union of any collection of open sets is open. This topology is the coarsest topology for which the neighborhood filter at $ a $ is at least as fine as $ f $.

gc_nhds theorem

(a : α) : GaloisConnection (nhdsAdjoint a) fun t => @nhds α t a

Full source

theorem gc_nhds (a : α) : GaloisConnection (nhdsAdjoint a) fun t => @nhds α t a := fun f t => by
  rw [le_nhds_iff]
  exact ⟨fun H s hs has => H _ has hs, fun H s has hs => H _ hs has⟩

Galois Connection Between Topologies and Neighborhood Filters at a Point

Informal description

For any point $a$ in a type $\alpha$, the pair of functions $(F, G)$ forms a Galois connection between topologies on $\alpha$ and filters on $\alpha$, where: - $F$ maps a filter $f$ to the topology `nhdsAdjoint a f` (the coarsest topology where the neighborhood filter at $a$ is at least as fine as $f$) - $G$ maps a topology $t$ to the neighborhood filter $\mathcal{N}_t(a)$ in that topology This means for any filter $f$ and topology $t$, we have: $F(f) \leq t \iff f \leq G(t)$ where the ordering on topologies is by reverse inclusion (finer topologies are larger) and the ordering on filters is by inclusion.

nhds_mono theorem

{t₁ t₂ : TopologicalSpace α} {a : α} (h : t₁ ≤ t₂) : @nhds α t₁ a ≤ @nhds α t₂ a

Full source

theorem nhds_mono {t₁ t₂ : TopologicalSpace α} {a : α} (h : t₁ ≤ t₂) :
    @nhds α t₁ a ≤ @nhds α t₂ a :=
  (gc_nhds a).monotone_u h

Monotonicity of Neighborhood Filters with Respect to Finer Topologies

Informal description

For any two topological spaces $t₁$ and $t₂$ on a type $\alpha$ and any point $a \in \alpha$, if $t₁$ is finer than $t₂$ (i.e., $t₁ \leq t₂$ in the partial order of topologies), then the neighborhood filter at $a$ in $t₁$ is finer than the neighborhood filter at $a$ in $t₂$ (i.e., $\mathcal{N}_{t₁}(a) \leq \mathcal{N}_{t₂}(a)$).

le_iff_nhds theorem

{α : Type*} (t t' : TopologicalSpace α) : t ≤ t' ↔ ∀ x, @nhds α t x ≤ @nhds α t' x

Full source

theorem le_iff_nhds {α : Type*} (t t' : TopologicalSpace α) :
    t ≤ t' ↔ ∀ x, @nhds α t x ≤ @nhds α t' x :=
  ⟨fun h _ => nhds_mono h, le_of_nhds_le_nhds⟩

Characterization of Finer Topology via Neighborhood Filters

Informal description

For any two topologies $t$ and $t'$ on a type $\alpha$, the topology $t$ is finer than $t'$ (i.e., $t \leq t'$) if and only if for every point $x \in \alpha$, the neighborhood filter $\mathcal{N}_t(x)$ in $t$ is finer than the neighborhood filter $\mathcal{N}_{t'}(x)$ in $t'$ (i.e., $\mathcal{N}_t(x) \leq \mathcal{N}_{t'}(x)$).

isOpen_singleton_nhdsAdjoint theorem

{α : Type*} {a b : α} (f : Filter α) (hb : b ≠ a) : IsOpen[nhdsAdjoint a f] { b }

Full source

theorem isOpen_singleton_nhdsAdjoint {α : Type*} {a b : α} (f : Filter α) (hb : b ≠ a) :
    IsOpen[nhdsAdjoint a f] {b} := fun h ↦
  absurd h hb.symm

Openness of Singleton Sets in `nhdsAdjoint` Topology for Distinct Points

Informal description

For any type $\alpha$ and distinct elements $a, b \in \alpha$, given a filter $f$ on $\alpha$, the singleton set $\{b\}$ is open in the topology `nhdsAdjoint a f`.

nhds_nhdsAdjoint_same theorem

(a : α) (f : Filter α) : @nhds α (nhdsAdjoint a f) a = pure a ⊔ f

Full source

theorem nhds_nhdsAdjoint_same (a : α) (f : Filter α) :
    @nhds α (nhdsAdjoint a f) a = purepure a ⊔ f := by
  let _ := nhdsAdjoint a f
  apply le_antisymm
  · rintro t ⟨hat : a ∈ t, htf : t ∈ f⟩
    exact IsOpen.mem_nhds (fun _ ↦ htf) hat
  · exact sup_le (pure_le_nhds _) ((gc_nhds a).le_u_l f)

Neighborhood Filter at Point in `nhdsAdjoint` Topology Equals Supremum of Principal Ultrafilter and Given Filter

Informal description

For any point $a$ in a type $\alpha$ and any filter $f$ on $\alpha$, the neighborhood filter of $a$ in the topology `nhdsAdjoint a f` is equal to the supremum of the principal ultrafilter at $a$ and the filter $f$, i.e., $\mathcal{N}_{\text{nhdsAdjoint}\,a\,f}(a) = \text{pure}\,a \sqcup f$.

nhds_nhdsAdjoint_of_ne theorem

{a b : α} (f : Filter α) (h : b ≠ a) : @nhds α (nhdsAdjoint a f) b = pure b

Full source

theorem nhds_nhdsAdjoint_of_ne {a b : α} (f : Filter α) (h : b ≠ a) :
    @nhds α (nhdsAdjoint a f) b = pure b :=
  let _ := nhdsAdjoint a f
  (isOpen_singleton_iff_nhds_eq_pure _).1 <| isOpen_singleton_nhdsAdjoint f h

Neighborhood Filter at Distinct Point in `nhdsAdjoint` Topology Equals Principal Ultrafilter

Informal description

For any distinct points $a$ and $b$ in a type $\alpha$ and any filter $f$ on $\alpha$, the neighborhood filter of $b$ in the topology `nhdsAdjoint a f` is equal to the principal ultrafilter at $b$, i.e., $\mathcal{N}_{\text{nhdsAdjoint}\,a\,f}(b) = \text{pure}\,b$.

nhds_nhdsAdjoint theorem

[DecidableEq α] (a : α) (f : Filter α) : @nhds α (nhdsAdjoint a f) = update pure a (pure a ⊔ f)

Full source

theorem nhds_nhdsAdjoint [DecidableEq α] (a : α) (f : Filter α) :
    @nhds α (nhdsAdjoint a f) = update pure a (purepure a ⊔ f) :=
  eq_update_iff.2 ⟨nhds_nhdsAdjoint_same .., fun _ ↦ nhds_nhdsAdjoint_of_ne _⟩

Neighborhood Filter Characterization in `nhdsAdjoint` Topology

Informal description

For a type $\alpha$ with decidable equality, a point $a \in \alpha$, and a filter $f$ on $\alpha$, the neighborhood filter function in the topology `nhdsAdjoint a f` is equal to the function obtained by updating the principal ultrafilter function at $a$ with the supremum of the principal ultrafilter at $a$ and $f$. That is, for any $x \in \alpha$, \[ \mathcal{N}_{\text{nhdsAdjoint}\,a\,f}(x) = \begin{cases} \text{pure}\,a \sqcup f & \text{if } x = a, \\ \text{pure}\,x & \text{otherwise.} \end{cases} \]

le_nhdsAdjoint_iff' theorem

 {a : α} {f : Filter α} {t : TopologicalSpace α} :
  t ≤ nhdsAdjoint a f ↔ @nhds α t a ≤ pure a ⊔ f ∧ ∀ b ≠ a, @nhds α t b = pure b

Full source

theorem le_nhdsAdjoint_iff' {a : α} {f : Filter α} {t : TopologicalSpace α} :
    t ≤ nhdsAdjoint a f ↔ @nhds α t a ≤ pure a ⊔ f ∧ ∀ b ≠ a, @nhds α t b = pure b := by
  classical
  simp_rw [le_iff_nhds, nhds_nhdsAdjoint, forall_update_iff, (pure_le_nhds _).le_iff_eq]

Characterization of Finer Topologies via `nhdsAdjoint`

Informal description

For a topological space $t$ on a type $\alpha$, a point $a \in \alpha$, and a filter $f$ on $\alpha$, the topology $t$ is finer than the topology `nhdsAdjoint a f` (i.e., $t \leq \text{nhdsAdjoint } a \ f$) if and only if: 1. The neighborhood filter of $a$ in $t$ is contained in the join of the principal ultrafilter at $a$ and $f$ (i.e., $\mathcal{N}_t(a) \leq \text{pure } a \sqcup f$), and 2. For every point $b \neq a$ in $\alpha$, the neighborhood filter of $b$ in $t$ is equal to the principal ultrafilter at $b$ (i.e., $\mathcal{N}_t(b) = \text{pure } b$).

le_nhdsAdjoint_iff theorem

 {α : Type*} (a : α) (f : Filter α) (t : TopologicalSpace α) :
  t ≤ nhdsAdjoint a f ↔ @nhds α t a ≤ pure a ⊔ f ∧ ∀ b ≠ a, IsOpen[t] { b }

Full source

theorem le_nhdsAdjoint_iff {α : Type*} (a : α) (f : Filter α) (t : TopologicalSpace α) :
    t ≤ nhdsAdjoint a f ↔ @nhds α t a ≤ pure a ⊔ f ∧ ∀ b ≠ a, IsOpen[t] {b} := by
  simp only [le_nhdsAdjoint_iff', @isOpen_singleton_iff_nhds_eq_pure α t]

Characterization of Finer Topologies via `nhdsAdjoint`

Informal description

Let $\alpha$ be a type, $a \in \alpha$ a point, $f$ a filter on $\alpha$, and $t$ a topology on $\alpha$. Then $t$ is finer than the topology `nhdsAdjoint a f` (i.e., $t \leq \text{nhdsAdjoint } a \ f$) if and only if: 1. The neighborhood filter of $a$ in $t$ is contained in the join of the principal ultrafilter at $a$ and $f$ (i.e., $\mathcal{N}_t(a) \leq \text{pure } a \sqcup f$), and 2. For every point $b \neq a$ in $\alpha$, the singleton set $\{b\}$ is open in the topology $t$.

nhds_iInf theorem

{ι : Sort*} {t : ι → TopologicalSpace α} {a : α} : @nhds α (iInf t) a = ⨅ i, @nhds α (t i) a

Full source

theorem nhds_iInf {ι : Sort*} {t : ι → TopologicalSpace α} {a : α} :
    @nhds α (iInf t) a = ⨅ i, @nhds α (t i) a :=
  (gc_nhds a).u_iInf

Neighborhood Filter of Infimum Topology Equals Infimum of Neighborhood Filters

Informal description

For any family of topologies $\{t_i\}_{i \in \iota}$ on a type $\alpha$ and any point $a \in \alpha$, the neighborhood filter at $a$ in the infimum topology $\bigsqcap_i t_i$ is equal to the infimum of the neighborhood filters at $a$ in each topology $t_i$. That is, $$\mathcal{N}_{\bigsqcap_i t_i}(a) = \bigsqcap_i \mathcal{N}_{t_i}(a).$$

nhds_sInf theorem

{s : Set (TopologicalSpace α)} {a : α} : @nhds α (sInf s) a = ⨅ t ∈ s, @nhds α t a

Full source

theorem nhds_sInf {s : Set (TopologicalSpace α)} {a : α} :
    @nhds α (sInf s) a = ⨅ t ∈ s, @nhds α t a :=
  (gc_nhds a).u_sInf

Neighborhood Filter of Infimum Topology Equals Infimum of Neighborhood Filters

Informal description

For any set $s$ of topologies on a type $\alpha$ and any point $a \in \alpha$, the neighborhood filter of $a$ in the infimum topology $\bigsqcap s$ is equal to the infimum of the neighborhood filters of $a$ in each topology $t \in s$. In symbols: $$\mathcal{N}_{\bigsqcap s}(a) = \bigsqcap_{t \in s} \mathcal{N}_t(a)$$

nhds_inf theorem

{t₁ t₂ : TopologicalSpace α} {a : α} : @nhds α (t₁ ⊓ t₂) a = @nhds α t₁ a ⊓ @nhds α t₂ a

Full source

theorem nhds_inf {t₁ t₂ : TopologicalSpace α} {a : α} :
    @nhds α (t₁ ⊓ t₂) a = @nhds α t₁ a ⊓ @nhds α t₂ a :=
  (gc_nhds a).u_inf (b₁ := t₁)

Neighborhood Filter of Infimum Topology Equals Infimum of Neighborhood Filters

Informal description

For any two topologies $t₁$ and $t₂$ on a type $\alpha$ and any point $a \in \alpha$, the neighborhood filter at $a$ in the infimum topology $t₁ \sqcap t₂$ is equal to the infimum of the neighborhood filters at $a$ in $t₁$ and $t₂$. That is, \[ \mathcal{N}_{t₁ \sqcap t₂}(a) = \mathcal{N}_{t₁}(a) \sqcap \mathcal{N}_{t₂}(a). \]

nhds_top theorem

{a : α} : @nhds α ⊤ a = ⊤

Full source

theorem nhds_top {a : α} : @nhds α ⊤ a = ⊤ :=
  (gc_nhds a).u_top

Neighborhood Filter in Indiscrete Topology is Trivial

Informal description

For any point $a$ in a type $\alpha$, the neighborhood filter at $a$ in the indiscrete topology (the coarsest topology on $\alpha$) is the trivial filter containing all subsets of $\alpha$, i.e., $\mathcal{N}_{\top}(a) = \top$.

isOpen_sup theorem

{t₁ t₂ : TopologicalSpace α} {s : Set α} : IsOpen[t₁ ⊔ t₂] s ↔ IsOpen[t₁] s ∧ IsOpen[t₂] s

Full source

theorem isOpen_sup {t₁ t₂ : TopologicalSpace α} {s : Set α} :
    IsOpen[t₁ ⊔ t₂]IsOpen[t₁ ⊔ t₂] s ↔ IsOpen[t₁] s ∧ IsOpen[t₂] s :=
  Iff.rfl

Open Sets in Supremum Topology are Open in Both Component Topologies

Informal description

Let $t₁$ and $t₂$ be two topologies on a type $\alpha$, and let $s$ be a subset of $\alpha$. Then $s$ is open in the supremum topology $t₁ ⊔ t₂$ if and only if $s$ is open in both $t₁$ and $t₂$.

continuous_iff_coinduced_le theorem

{t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} : Continuous[t₁, t₂] f ↔ coinduced f t₁ ≤ t₂

Full source

theorem continuous_iff_coinduced_le {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} :
    Continuous[t₁, t₂]Continuous[t₁, t₂] f ↔ coinduced f t₁ ≤ t₂ :=
  continuous_def

Characterization of Continuity via Coinduced Topology

Informal description

Let $X$ and $Y$ be topological spaces with topologies $t₁$ and $t₂$ respectively, and let $f : X \to Y$ be a function. Then $f$ is continuous if and only if the coinduced topology on $Y$ by $f$ from $t₁$ is coarser than $t₂$, i.e., $\text{coinduced}\, f\, t₁ \leq t₂$.

continuous_iff_le_induced theorem

{t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} : Continuous[t₁, t₂] f ↔ t₁ ≤ induced f t₂

Full source

theorem continuous_iff_le_induced {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace β} :
    Continuous[t₁, t₂]Continuous[t₁, t₂] f ↔ t₁ ≤ induced f t₂ :=
  Iff.trans continuous_iff_coinduced_le (gc_coinduced_induced f _ _)

Characterization of Continuity via Induced Topology

Informal description

Let $X$ and $Y$ be topological spaces with topologies $t₁$ and $t₂$ respectively, and let $f : X \to Y$ be a function. Then $f$ is continuous if and only if the topology $t₁$ on $X$ is finer than the topology induced on $X$ by $f$ from $t₂$, i.e., $t₁ \leq \text{induced}\, f\, t₂$.

continuous_generateFrom_iff theorem

{t : TopologicalSpace α} {b : Set (Set β)} : Continuous[t, generateFrom b] f ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s)

Full source

lemma continuous_generateFrom_iff {t : TopologicalSpace α} {b : Set (Set β)} :
    Continuous[t, generateFrom b]Continuous[t, generateFrom b] f ↔ ∀ s ∈ b, IsOpen (f ⁻¹' s) := by
  rw [continuous_iff_coinduced_le, le_generateFrom_iff_subset_isOpen]
  simp only [isOpen_coinduced, preimage_id', subset_def, mem_setOf]

Continuity Criterion for Functions into Generated Topology: $f$ continuous iff preimages of basic opens are open

Informal description

Let $X$ and $Y$ be topological spaces with $X$ having topology $t$ and $Y$ having the topology generated by a collection of sets $b$. A function $f : X \to Y$ is continuous if and only if the preimage $f^{-1}(s)$ is open in $X$ for every set $s$ in the collection $b$.

continuous_induced_dom theorem

{t : TopologicalSpace β} : Continuous[induced f t, t] f

Full source

@[continuity, fun_prop]
theorem continuous_induced_dom {t : TopologicalSpace β} : Continuous[induced f t, t] f :=
  continuous_iff_le_induced.2 le_rfl

Continuity of $f$ under its induced topology

Informal description

Let $X$ and $Y$ be topological spaces, and let $f : X \to Y$ be a function. If $X$ is equipped with the topology induced by $f$ from a topology $t$ on $Y$, then $f$ is continuous from $(X, \text{induced}\, f\, t)$ to $(Y, t)$.

continuous_induced_rng theorem

 {g : γ → α} {t₂ : TopologicalSpace β} {t₁ : TopologicalSpace γ} :
  Continuous[t₁, induced f t₂] g ↔ Continuous[t₁, t₂] (f ∘ g)

Full source

theorem continuous_induced_rng {g : γ → α} {t₂ : TopologicalSpace β} {t₁ : TopologicalSpace γ} :
    Continuous[t₁, induced f t₂]Continuous[t₁, induced f t₂] g ↔ Continuous[t₁, t₂] (f ∘ g) := by
  simp only [continuous_iff_le_induced, induced_compose]

Continuity under Induced Topology: $g$ continuous iff $f \circ g$ continuous

Informal description

Let $g : \gamma \to \alpha$ be a function between topological spaces, with $t_1$ a topology on $\gamma$ and $t_2$ a topology on $\beta$. Then $g$ is continuous from $t_1$ to the topology on $\alpha$ induced by $f : \alpha \to \beta$ and $t_2$ if and only if the composition $f \circ g$ is continuous from $t_1$ to $t_2$.

continuous_coinduced_rng theorem

{t : TopologicalSpace α} : Continuous[t, coinduced f t] f

Full source

theorem continuous_coinduced_rng {t : TopologicalSpace α} :
    Continuous[t, coinduced f t] f :=
  continuous_iff_coinduced_le.2 le_rfl

Continuity of $f$ into its coinduced topology

Informal description

Let $X$ be a topological space with topology $t$, and let $f : X \to Y$ be a function. Then $f$ is continuous from $(X, t)$ to $(Y, \text{coinduced}\, f\, t)$, where $\text{coinduced}\, f\, t$ is the coinduced topology on $Y$ by $f$ from $t$.

continuous_coinduced_dom theorem

 {g : β → γ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace γ} :
  Continuous[coinduced f t₁, t₂] g ↔ Continuous[t₁, t₂] (g ∘ f)

Full source

theorem continuous_coinduced_dom {g : β → γ} {t₁ : TopologicalSpace α} {t₂ : TopologicalSpace γ} :
    Continuous[coinduced f t₁, t₂]Continuous[coinduced f t₁, t₂] g ↔ Continuous[t₁, t₂] (g ∘ f) := by
  simp only [continuous_iff_coinduced_le, coinduced_compose]

Continuity of Compositions under Coinduced Topologies: $g$ continuous iff $g \circ f$ continuous

Informal description

Let $f : \alpha \to \beta$ and $g : \beta \to \gamma$ be functions between topological spaces. For any topology $t_1$ on $\alpha$ and any topology $t_2$ on $\gamma$, the function $g$ is continuous from the coinduced topology on $\beta$ (via $f$ and $t_1$) to $t_2$ if and only if the composition $g \circ f$ is continuous from $t_1$ to $t_2$.

continuous_le_dom theorem

 {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₁) (h₂ : Continuous[t₁, t₃] f) :
  Continuous[t₂, t₃] f

Full source

theorem continuous_le_dom {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₁)
    (h₂ : Continuous[t₁, t₃] f) : Continuous[t₂, t₃] f := by
  rw [continuous_iff_le_induced] at h₂ ⊢
  exact le_trans h₁ h₂

Continuity Preserved Under Finer Domain Topology

Informal description

Let $X$ and $Y$ be topological spaces with topologies $t_1$ and $t_2$ on $X$ and $t_3$ on $Y$. If $t_2$ is finer than $t_1$ (i.e., $t_2 \leq t_1$) and a function $f : X \to Y$ is continuous from $t_1$ to $t_3$, then $f$ is also continuous from $t_2$ to $t_3$.

continuous_le_rng theorem

 {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₃) (h₂ : Continuous[t₁, t₂] f) :
  Continuous[t₁, t₃] f

Full source

theorem continuous_le_rng {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} (h₁ : t₂ ≤ t₃)
    (h₂ : Continuous[t₁, t₂] f) : Continuous[t₁, t₃] f := by
  rw [continuous_iff_coinduced_le] at h₂ ⊢
  exact le_trans h₂ h₁

Continuity Preserved Under Coarser Topologies

Informal description

Let $X$ and $Y$ be topological spaces with topologies $t₁$ on $X$ and $t₂, t₃$ on $Y$. If $t₂$ is finer than $t₃$ (i.e., $t₂ \leq t₃$) and a function $f : X \to Y$ is continuous from $t₁$ to $t₂$, then $f$ is also continuous from $t₁$ to $t₃$.

continuous_sup_dom theorem

 {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
  Continuous[t₁ ⊔ t₂, t₃] f ↔ Continuous[t₁, t₃] f ∧ Continuous[t₂, t₃] f

Full source

theorem continuous_sup_dom {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
    Continuous[t₁ ⊔ t₂, t₃]Continuous[t₁ ⊔ t₂, t₃] f ↔ Continuous[t₁, t₃] f ∧ Continuous[t₂, t₃] f := by
  simp only [continuous_iff_le_induced, sup_le_iff]

Continuity Under Supremum of Domain Topologies

Informal description

Let $t_1$ and $t_2$ be topologies on a type $\alpha$, and let $t_3$ be a topology on a type $\beta$. A function $f : \alpha \to \beta$ is continuous with respect to the supremum topology $t_1 \sqcup t_2$ on $\alpha$ and $t_3$ on $\beta$ if and only if $f$ is continuous with respect to both $t_1$ and $t_3$, and with respect to $t_2$ and $t_3$.

continuous_sup_rng_left theorem

 {t₁ : TopologicalSpace α} {t₃ t₂ : TopologicalSpace β} : Continuous[t₁, t₂] f → Continuous[t₁, t₂ ⊔ t₃] f

Full source

theorem continuous_sup_rng_left {t₁ : TopologicalSpace α} {t₃ t₂ : TopologicalSpace β} :
    Continuous[t₁, t₂] f → Continuous[t₁, t₂ ⊔ t₃] f :=
  continuous_le_rng le_sup_left

Continuity Preserved Under Supremum of Topologies (Left)

Informal description

Let $X$ and $Y$ be topological spaces with topologies $t₁$ on $X$ and $t₂, t₃$ on $Y$. If a function $f : X \to Y$ is continuous from $t₁$ to $t₂$, then $f$ is also continuous from $t₁$ to the supremum topology $t₂ \sqcup t₃$ on $Y$.

continuous_sup_rng_right theorem

 {t₁ : TopologicalSpace α} {t₃ t₂ : TopologicalSpace β} : Continuous[t₁, t₃] f → Continuous[t₁, t₂ ⊔ t₃] f

Full source

theorem continuous_sup_rng_right {t₁ : TopologicalSpace α} {t₃ t₂ : TopologicalSpace β} :
    Continuous[t₁, t₃] f → Continuous[t₁, t₂ ⊔ t₃] f :=
  continuous_le_rng le_sup_right

Continuity Preserved Under Supremum of Topologies (Right)

Informal description

Let $X$ and $Y$ be topological spaces with topologies $t_1$ on $X$ and $t_2, t_3$ on $Y$. If a function $f : X \to Y$ is continuous from $t_1$ to $t_3$, then $f$ is also continuous from $t_1$ to the supremum topology $t_2 \sqcup t_3$ on $Y$.

continuous_sSup_dom theorem

 {T : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β} : Continuous[sSup T, t₂] f ↔ ∀ t ∈ T, Continuous[t, t₂] f

Full source

theorem continuous_sSup_dom {T : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β} :
    Continuous[sSup T, t₂]Continuous[sSup T, t₂] f ↔ ∀ t ∈ T, Continuous[t, t₂] f := by
  simp only [continuous_iff_le_induced, sSup_le_iff]

Continuity Criterion for Supremum Topology Domain

Informal description

Let $T$ be a set of topologies on a type $\alpha$ and $t_2$ be a topology on a type $\beta$. A function $f : \alpha \to \beta$ is continuous from the supremum topology $\bigsqcup T$ on $\alpha$ to $t_2$ if and only if for every topology $t \in T$, $f$ is continuous from $t$ to $t_2$.

continuous_sSup_rng theorem

 {t₁ : TopologicalSpace α} {t₂ : Set (TopologicalSpace β)} {t : TopologicalSpace β} (h₁ : t ∈ t₂)
  (hf : Continuous[t₁, t] f) : Continuous[t₁, sSup t₂] f

Full source

theorem continuous_sSup_rng {t₁ : TopologicalSpace α} {t₂ : Set (TopologicalSpace β)}
    {t : TopologicalSpace β} (h₁ : t ∈ t₂) (hf : Continuous[t₁, t] f) :
    Continuous[t₁, sSup t₂] f :=
  continuous_iff_coinduced_le.2 <| le_sSup_of_le h₁ <| continuous_iff_coinduced_le.1 hf

Continuity Preserved under Supremum of Topologies

Informal description

Let $X$ be a topological space with topology $t₁$, and let $\{t_i\}_{i \in I}$ be a collection of topologies on a space $Y$, with $t$ being one of them (i.e., $t \in \{t_i\}_{i \in I}$). If a function $f : X \to Y$ is continuous when $Y$ is equipped with the topology $t$, then $f$ is also continuous when $Y$ is equipped with the supremum topology $\sup \{t_i\}_{i \in I}$ (i.e., the coarsest topology finer than every $t_i$).

continuous_iSup_dom theorem

 {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β} : Continuous[iSup t₁, t₂] f ↔ ∀ i, Continuous[t₁ i, t₂] f

Full source

theorem continuous_iSup_dom {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β} :
    Continuous[iSup t₁, t₂]Continuous[iSup t₁, t₂] f ↔ ∀ i, Continuous[t₁ i, t₂] f := by
  simp only [continuous_iff_le_induced, iSup_le_iff]

Continuity under Supremum Topology: $\text{Continuous}(\bigsqcup_i t_i, t_2) \leftrightarrow \forall i, \text{Continuous}(t_i, t_2)$

Informal description

For a family of topologies $(t_i)_{i \in \iota}$ on a type $\alpha$ and a topology $t_2$ on a type $\beta$, a function $f : \alpha \to \beta$ is continuous when $\alpha$ is equipped with the supremum topology $\bigsqcup_i t_i$ and $\beta$ is equipped with $t_2$ if and only if $f$ is continuous for each individual topology $t_i$ on $\alpha$ and $t_2$ on $\beta$.

continuous_iSup_rng theorem

 {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β} {i : ι} (h : Continuous[t₁, t₂ i] f) :
  Continuous[t₁, iSup t₂] f

Full source

theorem continuous_iSup_rng {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β} {i : ι}
    (h : Continuous[t₁, t₂ i] f) : Continuous[t₁, iSup t₂] f :=
  continuous_sSup_rng ⟨i, rfl⟩ h

Continuity Preserved under Supremum of Codomain Topologies

Informal description

Let $t₁$ be a topology on a type $\alpha$, and let $(t₂_i)_{i \in \iota}$ be a family of topologies on a type $\beta$. If a function $f : \alpha \to \beta$ is continuous with respect to $t₁$ and some $t₂_i$, then $f$ is also continuous with respect to $t₁$ and the supremum topology $\bigsqcup_{i \in \iota} t₂_i$.

continuous_inf_rng theorem

 {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} :
  Continuous[t₁, t₂ ⊓ t₃] f ↔ Continuous[t₁, t₂] f ∧ Continuous[t₁, t₃] f

Full source

theorem continuous_inf_rng {t₁ : TopologicalSpace α} {t₂ t₃ : TopologicalSpace β} :
    Continuous[t₁, t₂ ⊓ t₃]Continuous[t₁, t₂ ⊓ t₃] f ↔ Continuous[t₁, t₂] f ∧ Continuous[t₁, t₃] f := by
  simp only [continuous_iff_coinduced_le, le_inf_iff]

Continuity Criterion for Infimum of Topologies

Informal description

Let $t₁$ be a topology on a type $\alpha$, and let $t₂$ and $t₃$ be topologies on a type $\beta$. A function $f : \alpha \to \beta$ is continuous when mapping from $t₁$ to the infimum topology $t₂ \sqcap t₃$ if and only if $f$ is continuous when mapping from $t₁$ to $t₂$ and from $t₁$ to $t₃$ separately.

continuous_inf_dom_left theorem

 {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} : Continuous[t₁, t₃] f → Continuous[t₁ ⊓ t₂, t₃] f

Full source

theorem continuous_inf_dom_left {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
    Continuous[t₁, t₃] f → Continuous[t₁ ⊓ t₂, t₃] f :=
  continuous_le_dom inf_le_left

Continuity Preserved Under Infimum Domain Topology (Left)

Informal description

Let $t_1$ and $t_2$ be topologies on a type $\alpha$, and let $t_3$ be a topology on $\beta$. If a function $f : \alpha \to \beta$ is continuous with respect to $t_1$ and $t_3$, then $f$ is also continuous with respect to the infimum topology $t_1 \sqcap t_2$ and $t_3$.

continuous_inf_dom_right theorem

 {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} : Continuous[t₂, t₃] f → Continuous[t₁ ⊓ t₂, t₃] f

Full source

theorem continuous_inf_dom_right {t₁ t₂ : TopologicalSpace α} {t₃ : TopologicalSpace β} :
    Continuous[t₂, t₃] f → Continuous[t₁ ⊓ t₂, t₃] f :=
  continuous_le_dom inf_le_right

Continuity Preserved Under Infimum Domain Topology (Right)

Informal description

Let $t_1$ and $t_2$ be topologies on a type $\alpha$, and let $t_3$ be a topology on a type $\beta$. If a function $f : \alpha \to \beta$ is continuous from $t_2$ to $t_3$, then $f$ is also continuous from the infimum topology $t_1 \sqcap t_2$ to $t_3$.

continuous_sInf_dom theorem

 {t₁ : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β} {t : TopologicalSpace α} (h₁ : t ∈ t₁) :
  Continuous[t, t₂] f → Continuous[sInf t₁, t₂] f

Full source

theorem continuous_sInf_dom {t₁ : Set (TopologicalSpace α)} {t₂ : TopologicalSpace β}
    {t : TopologicalSpace α} (h₁ : t ∈ t₁) :
    Continuous[t, t₂] f → Continuous[sInf t₁, t₂] f :=
  continuous_le_dom <| sInf_le h₁

Continuity Preserved Under Infimum of Domain Topologies

Informal description

Let $\{t_i\}_{i \in I}$ be a collection of topologies on a type $\alpha$, and let $t_2$ be a topology on $\beta$. For any topology $t \in \{t_i\}_{i \in I}$, if a function $f : \alpha \to \beta$ is continuous from $t$ to $t_2$, then $f$ is also continuous from the infimum topology $\bigsqcap \{t_i\}_{i \in I}$ to $t_2$.

continuous_sInf_rng theorem

 {t₁ : TopologicalSpace α} {T : Set (TopologicalSpace β)} : Continuous[t₁, sInf T] f ↔ ∀ t ∈ T, Continuous[t₁, t] f

Full source

theorem continuous_sInf_rng {t₁ : TopologicalSpace α} {T : Set (TopologicalSpace β)} :
    Continuous[t₁, sInf T]Continuous[t₁, sInf T] f ↔ ∀ t ∈ T, Continuous[t₁, t] f := by
  simp only [continuous_iff_coinduced_le, le_sInf_iff]

Continuity Criterion for Infimum of Topologies

Informal description

For a fixed topological space $t₁$ on $\alpha$ and a collection $T$ of topological spaces on $\beta$, a function $f : \alpha \to \beta$ is continuous from $t₁$ to the infimum topology $\bigsqcap T$ if and only if $f$ is continuous from $t₁$ to every topology $t \in T$.

continuous_iInf_dom theorem

 {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β} {i : ι} : Continuous[t₁ i, t₂] f → Continuous[iInf t₁, t₂] f

Full source

theorem continuous_iInf_dom {t₁ : ι → TopologicalSpace α} {t₂ : TopologicalSpace β} {i : ι} :
    Continuous[t₁ i, t₂] f → Continuous[iInf t₁, t₂] f :=
  continuous_le_dom <| iInf_le _ _

Continuity Preserved Under Infimum of Domain Topologies

Informal description

Let $\{t_i\}_{i \in \iota}$ be a family of topologies on a type $\alpha$, and let $t_2$ be a topology on $\beta$. If a function $f : \alpha \to \beta$ is continuous from $t_i$ to $t_2$ for some $i \in \iota$, then $f$ is also continuous from the infimum topology $\bigsqcap_{i \in \iota} t_i$ to $t_2$.

continuous_iInf_rng theorem

 {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β} : Continuous[t₁, iInf t₂] f ↔ ∀ i, Continuous[t₁, t₂ i] f

Full source

theorem continuous_iInf_rng {t₁ : TopologicalSpace α} {t₂ : ι → TopologicalSpace β} :
    Continuous[t₁, iInf t₂]Continuous[t₁, iInf t₂] f ↔ ∀ i, Continuous[t₁, t₂ i] f := by
  simp only [continuous_iff_coinduced_le, le_iInf_iff]

Continuity Criterion for Infimum of Topologies

Informal description

Let $t₁$ be a topology on a type $\alpha$ and $\{t₂_i\}_{i \in \iota}$ be a family of topologies on a type $\beta$. A function $f : \alpha \to \beta$ is continuous when $\alpha$ is equipped with $t₁$ and $\beta$ is equipped with the infimum topology $\bigsqcap_i t₂_i$ if and only if for every index $i$, $f$ is continuous when $\beta$ is equipped with $t₂_i$.

continuous_bot theorem

{t : TopologicalSpace β} : Continuous[⊥, t] f

Full source

@[continuity, fun_prop]
theorem continuous_bot {t : TopologicalSpace β} : Continuous[⊥, t] f :=
  continuous_iff_le_induced.2 bot_le

Continuity of Functions from Discrete Topology

Informal description

For any topological space $(β, t)$, every function $f : (α, ⊥) → (β, t)$ is continuous, where $⊥$ denotes the discrete topology on $α$.

continuous_top theorem

{t : TopologicalSpace α} : Continuous[t, ⊤] f

Full source

@[continuity, fun_prop]
theorem continuous_top {t : TopologicalSpace α} : Continuous[t, ⊤] f :=
  continuous_iff_coinduced_le.2 le_top

Continuity of Any Function into Indiscrete Topology

Informal description

For any topological space $(X, t)$ and any function $f : X \to Y$, the map $f$ is continuous when $Y$ is equipped with the indiscrete topology $\top$.

continuous_id_iff_le theorem

{t t' : TopologicalSpace α} : Continuous[t, t'] id ↔ t ≤ t'

Full source

theorem continuous_id_iff_le {t t' : TopologicalSpace α} : Continuous[t, t']Continuous[t, t'] id ↔ t ≤ t' :=
  @continuous_def _ _ t t' id

Continuity of Identity Map via Fineness of Topologies

Informal description

Let $t$ and $t'$ be two topologies on a type $\alpha$. The identity map $\text{id} : (\alpha, t) \to (\alpha, t')$ is continuous if and only if $t$ is finer than $t'$ (i.e., $t \leq t'$).

continuous_id_of_le theorem

{t t' : TopologicalSpace α} (h : t ≤ t') : Continuous[t, t'] id

Full source

theorem continuous_id_of_le {t t' : TopologicalSpace α} (h : t ≤ t') : Continuous[t, t'] id :=
  continuous_id_iff_le.2 h

Continuity of Identity Map under Finer Topology

Informal description

Let $t$ and $t'$ be two topologies on a type $\alpha$. If $t$ is finer than $t'$ (i.e., $t \leq t'$), then the identity map $\text{id} : (\alpha, t) \to (\alpha, t')$ is continuous.

mem_nhds_induced theorem

 [T : TopologicalSpace α] (f : β → α) (a : β) (s : Set β) :
  s ∈ @nhds β (TopologicalSpace.induced f T) a ↔ ∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s

Full source

theorem mem_nhds_induced [T : TopologicalSpace α] (f : β → α) (a : β) (s : Set β) :
    s ∈ @nhds β (TopologicalSpace.induced f T) as ∈ @nhds β (TopologicalSpace.induced f T) a ↔ ∃ u ∈ 𝓝 (f a), f ⁻¹' u ⊆ s := by
  letI := T.induced f
  simp_rw [mem_nhds_iff, isOpen_induced_iff]
  constructor
  · rintro ⟨u, usub, ⟨v, openv, rfl⟩, au⟩
    exact ⟨v, ⟨v, Subset.rfl, openv, au⟩, usub⟩
  · rintro ⟨u, ⟨v, vsubu, openv, amem⟩, finvsub⟩
    exact ⟨f ⁻¹' v, (Set.preimage_mono vsubu).trans finvsub, ⟨⟨v, openv, rfl⟩, amem⟩⟩

Neighborhood Criterion for Induced Topology

Informal description

Let $\alpha$ and $\beta$ be types with a topology $T$ on $\alpha$, and let $f : \beta \to \alpha$ be a function. For any point $a \in \beta$ and any subset $s \subseteq \beta$, the set $s$ is a neighborhood of $a$ in the topology induced by $f$ if and only if there exists a neighborhood $u$ of $f(a)$ in $\alpha$ such that the preimage $f^{-1}(u)$ is contained in $s$. In symbols: \[ s \in \mathcal{N}_{\text{ind}}(a) \iff \exists u \in \mathcal{N}(f(a)), f^{-1}(u) \subseteq s \] where $\mathcal{N}_{\text{ind}}(a)$ denotes the neighborhood filter of $a$ in the induced topology, and $\mathcal{N}(f(a))$ denotes the neighborhood filter of $f(a)$ in $\alpha$.

nhds_induced theorem

[T : TopologicalSpace α] (f : β → α) (a : β) : @nhds β (TopologicalSpace.induced f T) a = comap f (𝓝 (f a))

Full source

theorem nhds_induced [T : TopologicalSpace α] (f : β → α) (a : β) :
    @nhds β (TopologicalSpace.induced f T) a = comap f (𝓝 (f a)) := by
  ext s
  rw [mem_nhds_induced, mem_comap]

Neighborhood Filter Characterization for Induced Topology

Informal description

Let $\alpha$ and $\beta$ be topological spaces, with $T$ being the topology on $\alpha$. For any function $f : \beta \to \alpha$ and any point $a \in \beta$, the neighborhood filter of $a$ in the topology induced by $f$ is equal to the preimage of the neighborhood filter of $f(a)$ under $f$. In symbols: \[ \mathcal{N}_{\text{ind}}(a) = f^{-1}(\mathcal{N}(f(a))) \] where $\mathcal{N}_{\text{ind}}(a)$ denotes the neighborhood filter of $a$ in the induced topology, and $\mathcal{N}(f(a))$ denotes the neighborhood filter of $f(a)$ in $\alpha$.

induced_iff_nhds_eq theorem

 [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : β → α) : tβ = tα.induced f ↔ ∀ b, 𝓝 b = comap f (𝓝 <| f b)

Full source

theorem induced_iff_nhds_eq [tα : TopologicalSpace α] [tβ : TopologicalSpace β] (f : β → α) :
    tβ = tα.induced f ↔ ∀ b, 𝓝 b = comap f (𝓝 <| f b) := by
  simp only [ext_iff_nhds, nhds_induced]

Characterization of Induced Topology via Neighborhood Filters

Informal description

Let $\alpha$ and $\beta$ be topological spaces with topologies $t_\alpha$ and $t_\beta$ respectively. For a function $f : \beta \to \alpha$, the topology $t_\beta$ is equal to the topology induced by $f$ from $t_\alpha$ if and only if for every point $b \in \beta$, the neighborhood filter $\mathcal{N}(b)$ in $t_\beta$ is equal to the preimage under $f$ of the neighborhood filter $\mathcal{N}(f(b))$ in $t_\alpha$. In symbols: \[ t_\beta = \text{induced } f \, t_\alpha \iff \forall b \in \beta, \, \mathcal{N}(b) = f^{-1}(\mathcal{N}(f(b))) \]

map_nhds_induced_of_surjective theorem

 [T : TopologicalSpace α] {f : β → α} (hf : Surjective f) (a : β) :
  map f (@nhds β (TopologicalSpace.induced f T) a) = 𝓝 (f a)

Full source

theorem map_nhds_induced_of_surjective [T : TopologicalSpace α] {f : β → α} (hf : Surjective f)
    (a : β) : map f (@nhds β (TopologicalSpace.induced f T) a) = 𝓝 (f a) := by
  rw [nhds_induced, map_comap_of_surjective hf]

Surjective Function Preserves Neighborhood Filters in Induced Topology

Informal description

Let $\alpha$ and $\beta$ be topological spaces, with $T$ being the topology on $\alpha$. For a surjective function $f : \beta \to \alpha$ and any point $a \in \beta$, the image under $f$ of the neighborhood filter of $a$ in the induced topology on $\beta$ is equal to the neighborhood filter of $f(a)$ in $\alpha$. In symbols: \[ f_*(\mathcal{N}_{\text{ind}}(a)) = \mathcal{N}(f(a)) \] where $\mathcal{N}_{\text{ind}}(a)$ denotes the neighborhood filter of $a$ in the topology induced by $f$, and $\mathcal{N}(f(a))$ denotes the neighborhood filter of $f(a)$ in $\alpha$.

continuous_nhdsAdjoint_dom theorem

 [TopologicalSpace β] {f : α → β} {a : α} {l : Filter α} : Continuous[nhdsAdjoint a l, _] f ↔ Tendsto f l (𝓝 (f a))

Full source

theorem continuous_nhdsAdjoint_dom [TopologicalSpace β] {f : α → β} {a : α} {l : Filter α} :
    Continuous[nhdsAdjoint a l, _]Continuous[nhdsAdjoint a l, _] f ↔ Tendsto f l (𝓝 (f a)) := by
  simp_rw [continuous_iff_le_induced, gc_nhds _ _, nhds_induced, tendsto_iff_comap]

Continuity Criterion for Topology Adjoint to a Filter

Informal description

Let $\alpha$ and $\beta$ be topological spaces, with $f : \alpha \to \beta$ a function, $a \in \alpha$ a point, and $l$ a filter on $\alpha$. Then $f$ is continuous at $a$ when $\alpha$ is equipped with the topology `nhdsAdjoint a l` if and only if $f$ tends to $f(a)$ along the filter $l$. In symbols: \[ f \text{ is continuous in } \text{nhdsAdjoint } a \, l \iff \text{Tendsto } f \, l \, (\mathcal{N}(f(a))) \]

coinduced_nhdsAdjoint theorem

(f : α → β) (a : α) (l : Filter α) : coinduced f (nhdsAdjoint a l) = nhdsAdjoint (f a) (map f l)

Full source

theorem coinduced_nhdsAdjoint (f : α → β) (a : α) (l : Filter α) :
    coinduced f (nhdsAdjoint a l) = nhdsAdjoint (f a) (map f l) :=
  eq_of_forall_ge_iff fun _ ↦ by
    rw [gc_nhds, ← continuous_iff_coinduced_le, continuous_nhdsAdjoint_dom, Tendsto]

Coinduced Topology of Filter-Adjoint Topology Equals Filter-Adjoint Topology of Mapped Filter

Informal description

Let $f : \alpha \to \beta$ be a function, $a \in \alpha$ a point, and $l$ a filter on $\alpha$. Then the coinduced topology on $\beta$ by $f$ from the topology `nhdsAdjoint a l` on $\alpha$ is equal to the topology `nhdsAdjoint (f a) (map f l)` on $\beta$. In symbols: \[ \text{coinduced}\, f\, (\text{nhdsAdjoint}\, a\, l) = \text{nhdsAdjoint}\, (f a)\, (f_* l) \]

isOpen_induced_eq theorem

{s : Set α} : IsOpen[induced f t] s ↔ s ∈ preimage f '' {s | IsOpen s}

Full source

theorem isOpen_induced_eq {s : Set α} :
    IsOpen[induced f t]IsOpen[induced f t] s ↔ s ∈ preimage f '' { s | IsOpen s } :=
  Iff.rfl

Characterization of Open Sets in Induced Topology via Preimages

Informal description

A subset $s$ of $\alpha$ is open in the topology induced by a function $f : \alpha \to \beta$ and a topology $t$ on $\beta$ if and only if $s$ is the preimage under $f$ of some open set in $\beta$ with respect to $t$. In other words, $s$ is open in the induced topology if and only if there exists an open set $U$ in $\beta$ such that $s = f^{-1}(U)$.

isOpen_induced theorem

{s : Set β} (h : IsOpen s) : IsOpen[induced f t] (f ⁻¹' s)

Full source

theorem isOpen_induced {s : Set β} (h : IsOpen s) : IsOpen[induced f t] (f ⁻¹' s) :=
  ⟨s, h, rfl⟩

Preimage of Open Set is Open in Induced Topology

Informal description

For any open set $s$ in the topological space $\beta$ with topology $t$, the preimage $f^{-1}(s)$ is open in the induced topology on $\alpha$ generated by $f$ and $t$.

map_nhds_induced_eq theorem

(a : α) : map f (@nhds α (induced f t) a) = 𝓝[range f] f a

Full source

theorem map_nhds_induced_eq (a : α) : map f (@nhds α (induced f t) a) = 𝓝[range f] f a := by
  rw [nhds_induced, Filter.map_comap, nhdsWithin]

Image of Neighborhood Filter in Induced Topology Equals Restricted Neighborhood Filter

Informal description

For any point $a$ in a topological space $\alpha$ with the topology induced by a function $f : \alpha \to \beta$ and a topology $t$ on $\beta$, the image under $f$ of the neighborhood filter of $a$ is equal to the neighborhood filter of $f(a)$ restricted to the range of $f$. In symbols: \[ f_*(\mathcal{N}_{\text{ind}}(a)) = \mathcal{N}(f(a)) \cap \text{range}(f) \] where $\mathcal{N}_{\text{ind}}(a)$ denotes the neighborhood filter of $a$ in the induced topology, $\mathcal{N}(f(a))$ denotes the neighborhood filter of $f(a)$ in $\beta$, and $\text{range}(f)$ is the range of the function $f$.

map_nhds_induced_of_mem theorem

{a : α} (h : range f ∈ 𝓝 (f a)) : map f (@nhds α (induced f t) a) = 𝓝 (f a)

Full source

theorem map_nhds_induced_of_mem {a : α} (h : rangerange f ∈ 𝓝 (f a)) :
    map f (@nhds α (induced f t) a) = 𝓝 (f a) := by rw [nhds_induced, Filter.map_comap_of_mem h]

Neighborhood Filter Equality for Induced Topology When Range is a Neighborhood

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, with $t$ being the topology on $\beta$. For any point $a \in \alpha$, if the range of $f$ is a neighborhood of $f(a)$ in $\beta$, then the image under $f$ of the neighborhood filter of $a$ in the induced topology equals the neighborhood filter of $f(a)$ in $\beta$. In symbols, if $\text{range } f \in \mathcal{N}(f(a))$, then: \[ f_*(\mathcal{N}_{\text{ind}}(a)) = \mathcal{N}(f(a)) \] where $\mathcal{N}_{\text{ind}}(a)$ denotes the neighborhood filter of $a$ in the induced topology, and $\mathcal{N}(f(a))$ denotes the neighborhood filter of $f(a)$ in $\beta$.

closure_induced theorem

{f : α → β} {a : α} {s : Set α} : a ∈ @closure α (t.induced f) s ↔ f a ∈ closure (f '' s)

Full source

theorem closure_induced {f : α → β} {a : α} {s : Set α} :
    a ∈ @closure α (t.induced f) sa ∈ @closure α (t.induced f) s ↔ f a ∈ closure (f '' s) := by
  letI := t.induced f
  simp only [mem_closure_iff_frequently, nhds_induced, frequently_comap, mem_image, and_comm]

Closure Characterization in Induced Topology via Function Images

Informal description

Let $f : \alpha \to \beta$ be a function between topological spaces, with $\alpha$ equipped with the topology induced by $f$ from $\beta$. For any subset $s \subseteq \alpha$ and any point $a \in \alpha$, $a$ is in the closure of $s$ in the induced topology if and only if $f(a)$ is in the closure of the image $f(s)$ in $\beta$. In symbols: \[ a \in \overline{s}_{\text{ind}} \iff f(a) \in \overline{f(s)} \] where $\overline{s}_{\text{ind}}$ denotes the closure of $s$ in the induced topology on $\alpha$, and $\overline{f(s)}$ denotes the closure of $f(s)$ in $\beta$.

isClosed_induced_iff' theorem

{f : α → β} {s : Set α} : IsClosed[t.induced f] s ↔ ∀ a, f a ∈ closure (f '' s) → a ∈ s

Full source

theorem isClosed_induced_iff' {f : α → β} {s : Set α} :
    IsClosed[t.induced f]IsClosed[t.induced f] s ↔ ∀ a, f a ∈ closure (f '' s) → a ∈ s := by
  letI := t.induced f
  simp only [← closure_subset_iff_isClosed, subset_def, closure_induced]

Characterization of Closed Sets in Induced Topology via Function Images

Informal description

Let $f : \alpha \to \beta$ be a function and $s \subseteq \alpha$ a subset. Then $s$ is closed in the topology induced by $f$ on $\alpha$ if and only if for every $a \in \alpha$, if $f(a)$ is in the closure of $f(s)$ in $\beta$, then $a \in s$.

isOpen_singleton_true theorem

: IsOpen ({ True } : Set Prop)

Full source

@[simp]
theorem isOpen_singleton_true : IsOpen ({True} : Set Prop) :=
  TopologicalSpace.GenerateOpen.basic _ (mem_singleton _)

Openness of Singleton True in Sierpiński Topology

Informal description

The singleton set containing the proposition `True` is open in the Sierpiński topology on the type of propositions `Prop`.

nhds_true theorem

: 𝓝 True = pure True

Full source

@[simp]
theorem nhds_true : 𝓝 True = pure True :=
  le_antisymm (le_pure_iff.2 <| isOpen_singleton_true.mem_nhds <| mem_singleton _) (pure_le_nhds _)

Neighborhood Filter of True in Sierpiński Topology is Principal Ultrafilter

Informal description

In the Sierpiński topology on the type of propositions `Prop`, the neighborhood filter of the true proposition is equal to the principal ultrafilter at `True`, i.e., $\mathcal{N}(\text{True}) = \{\text{True}\}$.

nhds_false theorem

: 𝓝 False = ⊤

Full source

@[simp]
theorem nhds_false : 𝓝 False = ⊤ :=
  TopologicalSpace.nhds_generateFrom.trans <| by simp [@and_comm (_ ∈ _), iInter_and]

Neighborhood Filter of False in Sierpiński Topology is Trivial

Informal description

In the Sierpiński topology on the type of propositions `Prop`, the neighborhood filter of the false proposition is equal to the trivial filter, i.e., $\mathcal{N}(\text{False}) = \top$.

tendsto_nhds_true theorem

{l : Filter α} {p : α → Prop} : Tendsto p l (𝓝 True) ↔ ∀ᶠ x in l, p x

Full source

theorem tendsto_nhds_true {l : Filter α} {p : α → Prop} :
    TendstoTendsto p l (𝓝 True) ↔ ∀ᶠ x in l, p x := by simp

Characterization of Convergence to True in Sierpiński Topology

Informal description

For any filter $l$ on a type $\alpha$ and any predicate $p : \alpha \to \text{Prop}$, the function $p$ tends to $\text{True}$ with respect to the neighborhood filter $\mathcal{N}(\text{True})$ if and only if $p(x)$ holds for eventually all $x$ in $l$. In other words, $\text{Tendsto}\, p\, l\, \mathcal{N}(\text{True}) \leftrightarrow \forall^{\text{eventually}} x \in l, p(x)$.

tendsto_nhds_Prop theorem

{l : Filter α} {p : α → Prop} {q : Prop} : Tendsto p l (𝓝 q) ↔ (q → ∀ᶠ x in l, p x)

Full source

theorem tendsto_nhds_Prop {l : Filter α} {p : α → Prop} {q : Prop} :
    TendstoTendsto p l (𝓝 q) ↔ (q → ∀ᶠ x in l, p x) := by
  by_cases q <;> simp [*]

Characterization of Limit in Sierpiński Topology via Eventual Truth

Informal description

For any filter $l$ on a type $\alpha$, a function $p : \alpha \to \text{Prop}$, and a proposition $q$, the function $p$ tends to $q$ with respect to the neighborhood filter $\mathcal{N}(q)$ in the Sierpiński topology if and only if $q$ implies that $p(x)$ holds for all $x$ in a set that is eventually in $l$. In other words, $\lim_{l} p = q$ if and only if $q$ implies that $p(x)$ is true for all $x$ in some set that is eventually in $l$.

continuous_Prop theorem

{p : α → Prop} : Continuous p ↔ IsOpen {x | p x}

Full source

theorem continuous_Prop {p : α → Prop} : ContinuousContinuous p ↔ IsOpen { x | p x } := by
  simp only [continuous_iff_continuousAt, ContinuousAt, tendsto_nhds_Prop, isOpen_iff_mem_nhds]; rfl

Characterization of Continuous Predicates via Open Sets

Informal description

For any function $p : \alpha \to \text{Prop}$, $p$ is continuous (with respect to the Sierpiński topology on $\text{Prop}$) if and only if the set $\{x \mid p x\}$ is open in $\alpha$.

isOpen_iff_continuous_mem theorem

{s : Set α} : IsOpen s ↔ Continuous (· ∈ s)

Full source

theorem isOpen_iff_continuous_mem {s : Set α} : IsOpenIsOpen s ↔ Continuous (· ∈ s) :=
  continuous_Prop.symm

Openness Characterization via Continuous Membership Predicate

Informal description

A subset $s$ of a topological space $\alpha$ is open if and only if the membership predicate $(\cdot \in s) : \alpha \to \text{Prop}$ is continuous (with respect to the Sierpiński topology on $\text{Prop}$).

generateFrom_union theorem

(a₁ a₂ : Set (Set α)) : generateFrom (a₁ ∪ a₂) = generateFrom a₁ ⊓ generateFrom a₂

Full source

theorem generateFrom_union (a₁ a₂ : Set (Set α)) :
    generateFrom (a₁ ∪ a₂) = generateFromgenerateFrom a₁ ⊓ generateFrom a₂ :=
  (gc_generateFrom α).u_inf

Topology Generated by Union Equals Infimum of Generated Topologies

Informal description

For any two collections of subsets $a_1$ and $a_2$ of a type $\alpha$, the topology generated by their union $a_1 \cup a_2$ is equal to the infimum (meet) of the topologies generated by $a_1$ and $a_2$ separately. In other words: \[ \text{generateFrom}(a_1 \cup a_2) = \text{generateFrom}(a_1) \sqcap \text{generateFrom}(a_2). \]

setOf_isOpen_sup theorem

(t₁ t₂ : TopologicalSpace α) : {s | IsOpen[t₁ ⊔ t₂] s} = {s | IsOpen[t₁] s} ∩ {s | IsOpen[t₂] s}

Full source

theorem setOf_isOpen_sup (t₁ t₂ : TopologicalSpace α) :
    { s | IsOpen[t₁ ⊔ t₂] s } = { s | IsOpen[t₁] s }{ s | IsOpen[t₁] s } ∩ { s | IsOpen[t₂] s } :=
  rfl

Open Sets in Supremum Topology as Intersection of Open Sets

Informal description

For any two topologies $t_1$ and $t_2$ on a type $\alpha$, the collection of open sets in the supremum topology $t_1 \sqcup t_2$ is equal to the intersection of the collections of open sets in $t_1$ and $t_2$. In other words, a set $s \subseteq \alpha$ is open in $t_1 \sqcup t_2$ if and only if $s$ is open in both $t_1$ and $t_2$.

generateFrom_iUnion theorem

{f : ι → Set (Set α)} : generateFrom (⋃ i, f i) = ⨅ i, generateFrom (f i)

Full source

theorem generateFrom_iUnion {f : ι → Set (Set α)} :
    generateFrom (⋃ i, f i) = ⨅ i, generateFrom (f i) :=
  (gc_generateFrom α).u_iInf

Generation of Topology from Union Equals Infimum of Generated Topologies

Informal description

For any family of collections of subsets $\{f_i\}_{i \in \iota}$ of a type $\alpha$, the topology generated by the union $\bigcup_i f_i$ is equal to the infimum (in the lattice of topologies ordered by reverse inclusion) of the topologies generated by each $f_i$. In symbols: \[ \text{generateFrom}\left(\bigcup_{i} f_i\right) = \bigsqcap_{i} \text{generateFrom}(f_i) \]

setOf_isOpen_iSup theorem

{t : ι → TopologicalSpace α} : {s | IsOpen[⨆ i, t i] s} = ⋂ i, {s | IsOpen[t i] s}

Full source

theorem setOf_isOpen_iSup {t : ι → TopologicalSpace α} :
    { s | IsOpen[⨆ i, t i] s } = ⋂ i, { s | IsOpen[t i] s } :=
  (gc_generateFrom α).l_iSup

Open Sets in Supremum Topology as Intersection of Component Open Sets

Informal description

For a family of topologies $\{t_i\}_{i \in \iota}$ on a type $\alpha$, the collection of open sets in the supremum topology $\bigsqcup_i t_i$ is equal to the intersection of all collections of open sets in each individual topology $t_i$. That is, a set $s$ is open in $\bigsqcup_i t_i$ if and only if it is open in every $t_i$.

generateFrom_sUnion theorem

{S : Set (Set (Set α))} : generateFrom (⋃₀ S) = ⨅ s ∈ S, generateFrom s

Full source

theorem generateFrom_sUnion {S : Set (Set (Set α))} :
    generateFrom (⋃₀ S) = ⨅ s ∈ S, generateFrom s :=
  (gc_generateFrom α).u_sInf

Topology Generated by Union of Collections Equals Infimum of Generated Topologies

Informal description

For any collection $S$ of sets of subsets of a type $\alpha$, the topology generated by the union $\bigcup₀ S$ is equal to the infimum of the topologies generated by each set $s \in S$.

setOf_isOpen_sSup theorem

{T : Set (TopologicalSpace α)} : {s | IsOpen[sSup T] s} = ⋂ t ∈ T, {s | IsOpen[t] s}

Full source

theorem setOf_isOpen_sSup {T : Set (TopologicalSpace α)} :
    { s | IsOpen[sSup T] s } = ⋂ t ∈ T, { s | IsOpen[t] s } :=
  (gc_generateFrom α).l_sSup

Open Sets in Supremum Topology as Intersection of Open Sets

Informal description

For any collection $T$ of topologies on a type $\alpha$, the set of open sets in the supremum topology $\bigsqcup T$ is equal to the intersection of all sets that are open in each topology $t \in T$. In other words, a set $s$ is open in $\bigsqcup T$ if and only if $s$ is open in every topology $t \in T$.

generateFrom_union_isOpen theorem

(a b : TopologicalSpace α) : generateFrom ({s | IsOpen[a] s} ∪ {s | IsOpen[b] s}) = a ⊓ b

Full source

theorem generateFrom_union_isOpen (a b : TopologicalSpace α) :
    generateFrom ({ s | IsOpen[a] s }{ s | IsOpen[a] s } ∪ { s | IsOpen[b] s }) = a ⊓ b :=
  (gciGenerateFrom α).u_inf_l _ _

Generation of Infimum Topology from Union of Open Sets

Informal description

For any two topologies $a$ and $b$ on a type $\alpha$, the topology generated by the union of their open sets is equal to the infimum (meet) of $a$ and $b$ in the lattice of topologies, i.e., \[ \text{generateFrom} \left( \{s \mid \text{IsOpen}[a]\ s\} \cup \{s \mid \text{IsOpen}[b]\ s\} \right) = a \sqcap b. \]

generateFrom_iUnion_isOpen theorem

(f : ι → TopologicalSpace α) : generateFrom (⋃ i, {s | IsOpen[f i] s}) = ⨅ i, f i

Full source

theorem generateFrom_iUnion_isOpen (f : ι → TopologicalSpace α) :
    generateFrom (⋃ i, { s | IsOpen[f i] s }) = ⨅ i, f i :=
  (gciGenerateFrom α).u_iInf_l _

Generation of Infimum Topology from Union of Open Sets

Informal description

For any family of topologies $(f_i)_{i \in \iota}$ on a type $\alpha$, the topology generated by the union of all open sets in these topologies is equal to the infimum (greatest lower bound) of the family $(f_i)_{i \in \iota}$ in the lattice of topologies on $\alpha$. In other words, \[ \text{generateFrom}\left(\bigcup_{i \in \iota} \{s \mid \text{IsOpen}[f_i]\ s\}\right) = \bigsqcap_{i \in \iota} f_i. \]

generateFrom_inter theorem

(a b : TopologicalSpace α) : generateFrom ({s | IsOpen[a] s} ∩ {s | IsOpen[b] s}) = a ⊔ b

Full source

theorem generateFrom_inter (a b : TopologicalSpace α) :
    generateFrom ({ s | IsOpen[a] s }{ s | IsOpen[a] s } ∩ { s | IsOpen[b] s }) = a ⊔ b :=
  (gciGenerateFrom α).u_sup_l _ _

Topology Generated by Intersection of Open Sets Equals Supremum of Topologies

Informal description

For any two topologies $a$ and $b$ on a type $\alpha$, the topology generated by the intersection of their open sets is equal to the supremum (coarsest common refinement) of $a$ and $b$ in the lattice of topologies ordered by reverse inclusion. That is, \[ \text{generateFrom} \big( \{s \mid \text{IsOpen}[a]\ s\} \cap \{s \mid \text{IsOpen}[b]\ s\} \big) = a \sqcup b. \]

generateFrom_iInter theorem

(f : ι → TopologicalSpace α) : generateFrom (⋂ i, {s | IsOpen[f i] s}) = ⨆ i, f i

Full source

theorem generateFrom_iInter (f : ι → TopologicalSpace α) :
    generateFrom (⋂ i, { s | IsOpen[f i] s }) = ⨆ i, f i :=
  (gciGenerateFrom α).u_iSup_l _

Generation of Supremum Topology from Intersection of Open Sets

Informal description

For any family of topologies $(f_i)_{i \in \iota}$ on a type $\alpha$, the topology generated by the intersection of all open sets in these topologies is equal to the supremum (least upper bound) of the family $(f_i)_{i \in \iota}$ in the lattice of topologies on $\alpha$. In other words, \[ \text{generateFrom}\left(\bigcap_{i \in \iota} \{s \mid \text{IsOpen}[f_i]\ s\}\right) = \bigsqcup_{i \in \iota} f_i. \]

generateFrom_iInter_of_generateFrom_eq_self theorem

 (f : ι → Set (Set α)) (hf : ∀ i, {s | IsOpen[generateFrom (f i)] s} = f i) :
  generateFrom (⋂ i, f i) = ⨆ i, generateFrom (f i)

Full source

theorem generateFrom_iInter_of_generateFrom_eq_self (f : ι → Set (Set α))
    (hf : ∀ i, { s | IsOpen[generateFrom (f i)] s } = f i) :
    generateFrom (⋂ i, f i) = ⨆ i, generateFrom (f i) :=
  (gciGenerateFrom α).u_iSup_of_lu_eq_self f hf

Topology Generated by Intersection Equals Supremum of Generated Topologies

Informal description

Let $\{f_i\}_{i \in \iota}$ be a family of collections of subsets of a type $\alpha$ such that for each $i$, the topology generated by $f_i$ has exactly $f_i$ as its collection of open sets (i.e., $\{s \mid \text{IsOpen}[\text{generateFrom}(f_i)]\, s\} = f_i$). Then the topology generated by the intersection $\bigcap_i f_i$ is equal to the supremum (in the lattice of topologies ordered by reverse inclusion) of the topologies generated by each $f_i$. That is, \[ \text{generateFrom}\left(\bigcap_i f_i\right) = \bigsqcup_i \text{generateFrom}(f_i). \]

isOpen_iSup_iff theorem

{s : Set α} : IsOpen[⨆ i, t i] s ↔ ∀ i, IsOpen[t i] s

Full source

theorem isOpen_iSup_iff {s : Set α} : IsOpen[⨆ i, t i]IsOpen[⨆ i, t i] s ↔ ∀ i, IsOpen[t i] s :=
  show s ∈ {s | IsOpen[iSup t] s}s ∈ {s | IsOpen[iSup t] s} ↔ s ∈ { x : Set α | ∀ i : ι, IsOpen[t i] x } by
    simp [setOf_isOpen_iSup]

Characterization of Open Sets in Supremum Topology

Informal description

For a set $s$ in a topological space $\alpha$ and a family of topologies $(t_i)_{i \in I}$ on $\alpha$, the set $s$ is open in the supremum topology $\bigsqcup_i t_i$ if and only if $s$ is open in each topology $t_i$.

isOpen_sSup_iff theorem

{s : Set α} {T : Set (TopologicalSpace α)} : IsOpen[sSup T] s ↔ ∀ t ∈ T, IsOpen[t] s

Full source

theorem isOpen_sSup_iff {s : Set α} {T : Set (TopologicalSpace α)} :
    IsOpen[sSup T]IsOpen[sSup T] s ↔ ∀ t ∈ T, IsOpen[t] s := by
  simp only [sSup_eq_iSup, isOpen_iSup_iff]

Characterization of Open Sets in Supremum Topology via Collection of Topologies

Informal description

For a set $s$ in a topological space $\alpha$ and a collection $T$ of topologies on $\alpha$, the set $s$ is open in the supremum topology $\mathrm{sSup}\, T$ if and only if $s$ is open in every topology $t \in T$.

isClosed_iSup_iff theorem

{s : Set α} : IsClosed[⨆ i, t i] s ↔ ∀ i, IsClosed[t i] s

Full source

theorem isClosed_iSup_iff {s : Set α} : IsClosed[⨆ i, t i]IsClosed[⨆ i, t i] s ↔ ∀ i, IsClosed[t i] s := by
  simp only [← @isOpen_compl_iff _ _ (⨆ i, t i), ← @isOpen_compl_iff _ _ (t _), isOpen_iSup_iff]

Closedness in Supremum Topology Characterization

Informal description

For a set $s$ in a topological space $\alpha$ and a family of topologies $(t_i)_{i \in I}$ on $\alpha$, the set $s$ is closed in the supremum topology $\bigsqcup_i t_i$ if and only if $s$ is closed in each topology $t_i$.

isClosed_sSup_iff theorem

{s : Set α} {T : Set (TopologicalSpace α)} : IsClosed[sSup T] s ↔ ∀ t ∈ T, IsClosed[t] s

Full source

theorem isClosed_sSup_iff {s : Set α} {T : Set (TopologicalSpace α)} :
    IsClosed[sSup T]IsClosed[sSup T] s ↔ ∀ t ∈ T, IsClosed[t] s := by
  simp only [sSup_eq_iSup, isClosed_iSup_iff]

Closedness in Supremum Topology Characterization

Informal description

For a set $s$ in a topological space $\alpha$ and a collection $T$ of topologies on $\alpha$, the set $s$ is closed in the supremum topology $\bigsqcup T$ if and only if $s$ is closed in every topology $t \in T$.

Mathlib.Topology.Order

Implementation notes

Tags