Mathlib.Topology.Separation.Hausdorff

T2Space structure

(X : Type u) [TopologicalSpace X]

Full source

/-- A T₂ space, also known as a Hausdorff space, is one in which for every
  `x ≠ y` there exists disjoint open sets around `x` and `y`. This is
  the most widely used of the separation axioms. -/
@[mk_iff]
class T2Space (X : Type u) [TopologicalSpace X] : Prop where
  /-- Every two points in a Hausdorff space admit disjoint open neighbourhoods. -/
  t2 : Pairwise fun x y => ∃ u v : Set X, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Hausdorff space (T₂ space)

Informal description

A topological space $ X $ is called a T₂ space (or Hausdorff space) if for any two distinct points $ x, y \in X $, there exist disjoint open sets $ U $ and $ V $ such that $ x \in U $ and $ y \in V $. This means that any two distinct points can be separated by neighborhoods.

t2_separation theorem

[T2Space X] {x y : X} (h : x ≠ y) : ∃ u v : Set X, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Full source

/-- Two different points can be separated by open sets. -/
theorem t2_separation [T2Space X] {x y : X} (h : x ≠ y) :
    ∃ u v : Set X, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v :=
  T2Space.t2 h

Existence of Separating Open Sets in Hausdorff Spaces

Informal description

Let $ X $ be a Hausdorff space. For any two distinct points $ x, y \in X $, there exist disjoint open sets $ U $ and $ V $ such that $ x \in U $ and $ y \in V $.

t2Space_iff_disjoint_nhds theorem

: T2Space X ↔ Pairwise fun x y : X => Disjoint (𝓝 x) (𝓝 y)

Full source

theorem t2Space_iff_disjoint_nhds : T2SpaceT2Space X ↔ Pairwise fun x y : X => Disjoint (𝓝 x) (𝓝 y) := by
  refine (t2Space_iff X).trans (forall₃_congr fun x y _ => ?_)
  simp only [(nhds_basis_opens x).disjoint_iff (nhds_basis_opens y), exists_prop, ← exists_and_left,
    and_assoc, and_comm, and_left_comm]

Characterization of Hausdorff Spaces via Disjoint Neighborhood Filters

Informal description

A topological space $X$ is Hausdorff (T₂) if and only if for every pair of distinct points $x, y \in X$, the neighborhood filters $\mathcal{N}(x)$ and $\mathcal{N}(y)$ are disjoint.

disjoint_nhds_nhds theorem

[T2Space X] {x y : X} : Disjoint (𝓝 x) (𝓝 y) ↔ x ≠ y

Full source

@[simp]
theorem disjoint_nhds_nhds [T2Space X] {x y : X} : DisjointDisjoint (𝓝 x) (𝓝 y) ↔ x ≠ y :=
  ⟨fun hd he => by simp [he, nhds_neBot.ne] at hd, (t2Space_iff_disjoint_nhds.mp ‹_› ·)⟩

Disjoint Neighborhood Filters Criterion for Distinct Points in Hausdorff Spaces

Informal description

In a Hausdorff space $X$, the neighborhood filters $\mathcal{N}(x)$ and $\mathcal{N}(y)$ of two points $x, y \in X$ are disjoint if and only if $x \neq y$.

pairwise_disjoint_nhds theorem

[T2Space X] : Pairwise (Disjoint on (𝓝 : X → Filter X))

Full source

theorem pairwise_disjoint_nhds [T2Space X] : Pairwise (DisjointDisjoint on (𝓝 : X → Filter X)) := fun _ _ =>
  disjoint_nhds_nhds.2

Pairwise Disjoint Neighborhood Filters in Hausdorff Spaces

Informal description

In a Hausdorff space $X$, the neighborhood filters $\mathcal{N}(x)$ for all points $x \in X$ are pairwise disjoint. That is, for any two distinct points $x, y \in X$, the filters $\mathcal{N}(x)$ and $\mathcal{N}(y)$ are disjoint.

Set.pairwiseDisjoint_nhds theorem

[T2Space X] (s : Set X) : s.PairwiseDisjoint 𝓝

Full source

protected theorem Set.pairwiseDisjoint_nhds [T2Space X] (s : Set X) : s.PairwiseDisjoint 𝓝 :=
  pairwise_disjoint_nhds.set_pairwise s

Pairwise Disjoint Neighborhood Filters on Subsets of Hausdorff Spaces

Informal description

For any subset $s$ of a Hausdorff space $X$, the neighborhood filters $\mathcal{N}(x)$ for all points $x \in s$ are pairwise disjoint. That is, for any two distinct points $x, y \in s$, the filters $\mathcal{N}(x)$ and $\mathcal{N}(y)$ are disjoint.

Set.Finite.t2_separation theorem

 [T2Space X] {s : Set X} (hs : s.Finite) : ∃ U : X → Set X, (∀ x, x ∈ U x ∧ IsOpen (U x)) ∧ s.PairwiseDisjoint U

Full source

/-- Points of a finite set can be separated by open sets from each other. -/
theorem Set.Finite.t2_separation [T2Space X] {s : Set X} (hs : s.Finite) :
    ∃ U : X → Set X, (∀ x, x ∈ U x ∧ IsOpen (U x)) ∧ s.PairwiseDisjoint U :=
  s.pairwiseDisjoint_nhds.exists_mem_filter_basis hs nhds_basis_opens

Finite Sets in Hausdorff Spaces Have Pairwise Disjoint Open Neighborhoods

Informal description

In a Hausdorff space $X$, for any finite subset $s \subseteq X$, there exists a family of open sets $(U_x)_{x \in s}$ such that each $U_x$ contains $x$ and the sets $U_x$ are pairwise disjoint for distinct points in $s$.

T2Space.t1Space instance

[T2Space X] : T1Space X

Full source

instance (priority := 100) T2Space.t1Space [T2Space X] : T1Space X :=
  t1Space_iff_disjoint_pure_nhds.mpr fun _ _ hne =>
    (disjoint_nhds_nhds.2 hne).mono_left <| pure_le_nhds _

Hausdorff Spaces are T₁ Spaces

Informal description

Every Hausdorff space is a T₁ space.

T2Space.r1Space instance

[T2Space X] : R1Space X

Full source

instance (priority := 100) T2Space.r1Space [T2Space X] : R1Space X :=
  ⟨fun x y ↦ (eq_or_ne x y).imp specializes_of_eq disjoint_nhds_nhds.2⟩

Hausdorff Spaces are R₁ Spaces

Informal description

Every Hausdorff space is an R₁ space.

SeparationQuotient.t2Space_iff theorem

: T2Space (SeparationQuotient X) ↔ R1Space X

Full source

theorem SeparationQuotient.t2Space_iff : T2SpaceT2Space (SeparationQuotient X) ↔ R1Space X := by
  simp only [t2Space_iff_disjoint_nhds, Pairwise, surjective_mk.forall₂, ne_eq, mk_eq_mk,
    r1Space_iff_inseparable_or_disjoint_nhds, ← disjoint_comap_iff surjective_mk, comap_mk_nhds_mk,
    ← or_iff_not_imp_left]

T₂ Property of Separation Quotient Equivalent to R₁ Property of Original Space

Informal description

The separation quotient of a topological space $X$ is a T₂ (Hausdorff) space if and only if $X$ is an R₁ space.

SeparationQuotient.t2Space instance

[R1Space X] : T2Space (SeparationQuotient X)

Full source

instance SeparationQuotient.t2Space [R1Space X] : T2Space (SeparationQuotient X) :=
  t2Space_iff.2 ‹_›

Separation Quotient of R₁ Space is Hausdorff

Informal description

For any topological space $X$ that is an R₁ space, its separation quotient is a Hausdorff (T₂) space.

instT2SpaceOfR1SpaceOfT0Space instance

[R1Space X] [T0Space X] : T2Space X

Full source

instance (priority := 80) [R1Space X] [T0Space X] : T2Space X :=
  t2Space_iff_disjoint_nhds.2 fun _x _y hne ↦ disjoint_nhds_nhds_iff_not_inseparable.2 fun hxy ↦
    hne hxy.eq

R₁ and T₀ Implies Hausdorff

Informal description

Every topological space $X$ that is both an R₁ space and a T₀ space is also a Hausdorff (T₂) space.

R1Space.t2Space_iff_t0Space theorem

[R1Space X] : T2Space X ↔ T0Space X

Full source

theorem R1Space.t2Space_iff_t0Space [R1Space X] : T2SpaceT2Space X ↔ T0Space X := by
  constructor <;> intro <;> infer_instance

Hausdorff Equivalence for R₁ Spaces: T₂ iff T₀

Informal description

For any topological space $X$ that is an R₁ space, $X$ is a Hausdorff (T₂) space if and only if it is a T₀ space.

t2_iff_nhds theorem

: T2Space X ↔ ∀ {x y : X}, NeBot (𝓝 x ⊓ 𝓝 y) → x = y

Full source

/-- A space is T₂ iff the neighbourhoods of distinct points generate the bottom filter. -/
theorem t2_iff_nhds : T2SpaceT2Space X ↔ ∀ {x y : X}, NeBot (𝓝 x ⊓ 𝓝 y) → x = y := by
  simp only [t2Space_iff_disjoint_nhds, disjoint_iff, neBot_iff, Ne, not_imp_comm, Pairwise]

Characterization of Hausdorff Spaces via Neighborhood Filters

Informal description

A topological space $X$ is a Hausdorff (T₂) space if and only if for any two distinct points $x, y \in X$, the intersection of their neighborhood filters $\mathcal{N}(x) \sqcap \mathcal{N}(y)$ is not a nontrivial filter (i.e., it implies $x = y$).

t2Space_iff_nhds theorem

: T2Space X ↔ Pairwise fun x y : X => ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V

Full source

theorem t2Space_iff_nhds :
    T2SpaceT2Space X ↔ Pairwise fun x y : X => ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V := by
  simp only [t2Space_iff_disjoint_nhds, Filter.disjoint_iff, Pairwise]

Characterization of Hausdorff Spaces via Disjoint Neighborhoods

Informal description

A topological space $X$ is a Hausdorff (T₂) space if and only if for every pair of distinct points $x, y \in X$, there exist neighborhoods $U$ of $x$ and $V$ of $y$ such that $U$ and $V$ are disjoint.

t2_separation_nhds theorem

[T2Space X] {x y : X} (h : x ≠ y) : ∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ Disjoint u v

Full source

theorem t2_separation_nhds [T2Space X] {x y : X} (h : x ≠ y) :
    ∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ Disjoint u v :=
  let ⟨u, v, open_u, open_v, x_in, y_in, huv⟩ := t2_separation h
  ⟨u, v, open_u.mem_nhds x_in, open_v.mem_nhds y_in, huv⟩

Existence of Disjoint Neighborhoods in Hausdorff Spaces

Informal description

Let $ X $ be a Hausdorff space. For any two distinct points $ x, y \in X $, there exist neighborhoods $ U $ of $ x $ and $ V $ of $ y $ such that $ U $ and $ V $ are disjoint.

t2_separation_compact_nhds theorem

 [LocallyCompactSpace X] [T2Space X] {x y : X} (h : x ≠ y) :
  ∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v

Full source

theorem t2_separation_compact_nhds [LocallyCompactSpace X] [T2Space X] {x y : X} (h : x ≠ y) :
    ∃ u v, u ∈ 𝓝 x ∧ v ∈ 𝓝 y ∧ IsCompact u ∧ IsCompact v ∧ Disjoint u v := by
  simpa only [exists_prop, ← exists_and_left, and_comm, and_assoc, and_left_comm] using
    ((compact_basis_nhds x).disjoint_iff (compact_basis_nhds y)).1 (disjoint_nhds_nhds.2 h)

Existence of disjoint compact neighborhoods in locally compact Hausdorff spaces

Informal description

Let $X$ be a locally compact Hausdorff space. For any two distinct points $x, y \in X$, there exist compact neighborhoods $u$ of $x$ and $v$ of $y$ such that $u$ and $v$ are disjoint.

t2_iff_ultrafilter theorem

: T2Space X ↔ ∀ {x y : X} (f : Ultrafilter X), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y

Full source

theorem t2_iff_ultrafilter :
    T2SpaceT2Space X ↔ ∀ {x y : X} (f : Ultrafilter X), ↑f ≤ 𝓝 x → ↑f ≤ 𝓝 y → x = y :=
  t2_iff_nhds.trans <| by simp only [← exists_ultrafilter_iff, and_imp, le_inf_iff, exists_imp]

Characterization of Hausdorff Spaces via Ultrafilter Convergence

Informal description

A topological space $X$ is Hausdorff (T₂) if and only if for any two points $x, y \in X$ and any ultrafilter $f$ on $X$, if $f$ converges to both $x$ and $y$, then $x = y$.

t2_iff_isClosed_diagonal theorem

: T2Space X ↔ IsClosed (diagonal X)

Full source

theorem t2_iff_isClosed_diagonal : T2SpaceT2Space X ↔ IsClosed (diagonal X) := by
  simp only [t2Space_iff_disjoint_nhds, ← isOpen_compl_iff, isOpen_iff_mem_nhds, Prod.forall,
    nhds_prod_eq, compl_diagonal_mem_prod, mem_compl_iff, mem_diagonal_iff, Pairwise]

Characterization of Hausdorff Spaces via Closed Diagonal

Informal description

A topological space $X$ is a Hausdorff space (T₂ space) if and only if the diagonal $\Delta_X = \{(x, x) \mid x \in X\}$ is closed in the product space $X \times X$.

isClosed_diagonal theorem

[T2Space X] : IsClosed (diagonal X)

Full source

theorem isClosed_diagonal [T2Space X] : IsClosed (diagonal X) :=
  t2_iff_isClosed_diagonal.mp ‹_›

Diagonal is Closed in Hausdorff Space

Informal description

In a Hausdorff space $X$, the diagonal $\Delta_X = \{(x, x) \mid x \in X\}$ is a closed subset of $X \times X$.

tendsto_nhds_unique theorem

 [T2Space X] {f : Y → X} {l : Filter Y} {a b : X} [NeBot l] (ha : Tendsto f l (𝓝 a)) (hb : Tendsto f l (𝓝 b)) : a = b

Full source

theorem tendsto_nhds_unique [T2Space X] {f : Y → X} {l : Filter Y} {a b : X} [NeBot l]
    (ha : Tendsto f l (𝓝 a)) (hb : Tendsto f l (𝓝 b)) : a = b :=
  (tendsto_nhds_unique_inseparable ha hb).eq

Uniqueness of Limits in Hausdorff Spaces

Informal description

Let $X$ be a Hausdorff space, $Y$ a topological space, and $f : Y \to X$ a function. For any filter $l$ on $Y$ that is not the trivial filter, if $f$ tends to both $a$ and $b$ in $X$ along $l$, then $a = b$.

tendsto_nhds_unique' theorem

 [T2Space X] {f : Y → X} {l : Filter Y} {a b : X} (_ : NeBot l) (ha : Tendsto f l (𝓝 a)) (hb : Tendsto f l (𝓝 b)) :
  a = b

Full source

theorem tendsto_nhds_unique' [T2Space X] {f : Y → X} {l : Filter Y} {a b : X} (_ : NeBot l)
    (ha : Tendsto f l (𝓝 a)) (hb : Tendsto f l (𝓝 b)) : a = b :=
  tendsto_nhds_unique ha hb

Uniqueness of Limits in Hausdorff Spaces (Primed Version)

Informal description

Let $X$ be a Hausdorff space, $Y$ a topological space, and $f : Y \to X$ a function. For any filter $l$ on $Y$ that is not the trivial filter, if $f$ tends to both $a$ and $b$ in $X$ along $l$, then $a = b$.

tendsto_nhds_unique_of_eventuallyEq theorem

 [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X} [NeBot l] (ha : Tendsto f l (𝓝 a)) (hb : Tendsto g l (𝓝 b))
  (hfg : f =ᶠ[l] g) : a = b

Full source

theorem tendsto_nhds_unique_of_eventuallyEq [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X}
    [NeBot l] (ha : Tendsto f l (𝓝 a)) (hb : Tendsto g l (𝓝 b)) (hfg : f =ᶠ[l] g) : a = b :=
  tendsto_nhds_unique (ha.congr' hfg) hb

Uniqueness of Limits in Hausdorff Spaces under Eventual Equality

Informal description

Let $X$ be a Hausdorff space, $Y$ a topological space, and $f, g : Y \to X$ functions. For any filter $l$ on $Y$ that is not the trivial filter, if $f$ tends to $a$ and $g$ tends to $b$ along $l$, and $f$ and $g$ are eventually equal along $l$, then $a = b$.

tendsto_nhds_unique_of_frequently_eq theorem

 [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X} (ha : Tendsto f l (𝓝 a)) (hb : Tendsto g l (𝓝 b))
  (hfg : ∃ᶠ x in l, f x = g x) : a = b

Full source

theorem tendsto_nhds_unique_of_frequently_eq [T2Space X] {f g : Y → X} {l : Filter Y} {a b : X}
    (ha : Tendsto f l (𝓝 a)) (hb : Tendsto g l (𝓝 b)) (hfg : ∃ᶠ x in l, f x = g x) : a = b :=
  have : ∃ᶠ z : X × X in 𝓝 (a, b), z.1 = z.2 := (ha.prodMk_nhds hb).frequently hfg
  not_not.1 fun hne => this (isClosed_diagonal.isOpen_compl.mem_nhds hne)

Uniqueness of Limits in Hausdorff Spaces under Frequent Coincidence

Informal description

Let $X$ be a Hausdorff space, and let $f, g : Y \to X$ be functions. Suppose $f$ tends to $a$ and $g$ tends to $b$ along a filter $l$ on $Y$. If there exists a set in $l$ where $f$ and $g$ coincide frequently (i.e., for infinitely many points in $l$), then $a = b$.

IsCompact.nhdsSet_inter_eq theorem

[T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) : 𝓝ˢ (s ∩ t) = 𝓝ˢ s ⊓ 𝓝ˢ t

Full source

/-- If `s` and `t` are compact sets in a T₂ space, then the set neighborhoods filter of `s ∩ t`
is the infimum of set neighborhoods filters for `s` and `t`.

For general sets, only the `≤` inequality holds, see `nhdsSet_inter_le`. -/
theorem IsCompact.nhdsSet_inter_eq [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) :
    𝓝ˢ (s ∩ t) = 𝓝ˢ𝓝ˢ s ⊓ 𝓝ˢ t := by
  refine le_antisymm (nhdsSet_inter_le _ _) ?_
  simp_rw [hs.nhdsSet_inf_eq_biSup, ht.inf_nhdsSet_eq_biSup, nhdsSet, sSup_image]
  refine iSup₂_le fun x hxs ↦ iSup₂_le fun y hyt ↦ ?_
  rcases eq_or_ne x y with (rfl|hne)
  · exact le_iSup₂_of_le x ⟨hxs, hyt⟩ (inf_idem _).le
  · exact (disjoint_nhds_nhds.mpr hne).eq_bot ▸ bot_le

Neighborhood Filter of Intersection of Compact Sets in Hausdorff Space Equals Infimum of Individual Neighborhood Filters

Informal description

Let $X$ be a Hausdorff space, and let $s, t \subseteq X$ be compact subsets. Then the neighborhood filter of the intersection $s \cap t$ is equal to the infimum of the neighborhood filters of $s$ and $t$, i.e., \[ \mathcal{N}^s(s \cap t) = \mathcal{N}^s(s) \sqcap \mathcal{N}^s(t). \]

IsCompact.separation_of_not_mem theorem

 {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) :
  ∃ (U : Set X), ∃ (V : Set X), IsOpen U ∧ IsOpen V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V

Full source

/-- In a `T2Space X`, for a compact set `t` and a point `x` outside `t`, there are open sets `U`,
`V` that separate `t` and `x`. -/
lemma IsCompact.separation_of_not_mem {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X}
    {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) :
    ∃ (U : Set X), ∃ (V : Set X), IsOpen U ∧ IsOpen V ∧ t ⊆ U ∧ x ∈ V ∧ Disjoint U V := by
  simpa [SeparatedNhds] using SeparatedNhds.of_isCompact_isCompact_isClosed H1 isCompact_singleton
    isClosed_singleton <| disjoint_singleton_right.mpr H2

Separation of Compact Set and Point in Hausdorff Space

Informal description

Let $X$ be a Hausdorff space, $t \subseteq X$ a compact subset, and $x \in X$ a point not in $t$. Then there exist disjoint open sets $U$ and $V$ such that $t \subseteq U$ and $x \in V$.

IsCompact.disjoint_nhdsSet_nhds theorem

 {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X} {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) :
  Disjoint (𝓝ˢ t) (𝓝 x)

Full source

/-- In a `T2Space X`, for a compact set `t` and a point `x` outside `t`, `𝓝ˢ t` and `𝓝 x` are
disjoint. -/
lemma IsCompact.disjoint_nhdsSet_nhds {X : Type u_1} [TopologicalSpace X] [T2Space X] {x : X}
    {t : Set X} (H1 : IsCompact t) (H2 : x ∉ t) :
    Disjoint (𝓝ˢ t) (𝓝 x) := by
  simpa using SeparatedNhds.disjoint_nhdsSet <| .of_isCompact_isCompact_isClosed H1
    isCompact_singleton isClosed_singleton <| disjoint_singleton_right.mpr H2

Disjointness of Neighborhood Filters for Compact Sets in Hausdorff Spaces

Informal description

Let $X$ be a Hausdorff topological space, $t \subseteq X$ a compact subset, and $x \in X$ a point not in $t$. Then the neighborhood filter $\mathcal{N}^s(t)$ of $t$ and the neighborhood filter $\mathcal{N}(x)$ of $x$ are disjoint.

Set.InjOn.exists_mem_nhdsSet theorem

 {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} {s : Set X} (inj : InjOn f s)
  (sc : IsCompact s) (fc : ∀ x ∈ s, ContinuousAt f x) (loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u) : ∃ t ∈ 𝓝ˢ s, InjOn f t

Full source

/-- If a function `f` is

- injective on a compact set `s`;
- continuous at every point of this set;
- injective on a neighborhood of each point of this set,

then it is injective on a neighborhood of this set. -/
theorem Set.InjOn.exists_mem_nhdsSet {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [T2Space Y] {f : X → Y} {s : Set X} (inj : InjOn f s) (sc : IsCompact s)
    (fc : ∀ x ∈ s, ContinuousAt f x) (loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u) :
    ∃ t ∈ 𝓝ˢ s, InjOn f t := by
  have : ∀ x ∈ s ×ˢ s, ∀ᶠ y in 𝓝 x, f y.1 = f y.2 → y.1 = y.2 := fun (x, y) ⟨hx, hy⟩ ↦ by
    rcases eq_or_ne x y with rfl | hne
    · rcases loc x hx with ⟨u, hu, hf⟩
      exact Filter.mem_of_superset (prod_mem_nhds hu hu) <| forall_prod_set.2 hf
    · suffices ∀ᶠ z in 𝓝 (x, y), f z.1 ≠ f z.2 from this.mono fun _ hne h ↦ absurd h hne
      refine (fc x hx).prodMap' (fc y hy) <| isClosed_diagonal.isOpen_compl.mem_nhds ?_
      exact inj.ne hx hy hne
  rw [← eventually_nhdsSet_iff_forall, sc.nhdsSet_prod_eq sc] at this
  exact eventually_prod_self_iff.1 this

Local Injectivity Extension for Functions on Compact Sets in Hausdorff Spaces

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ Hausdorff, and let $f : X \to Y$ be a function. Suppose that: 1. $f$ is injective on a compact subset $s \subseteq X$; 2. $f$ is continuous at every point of $s$; 3. For each $x \in s$, there exists a neighborhood $u$ of $x$ such that $f$ is injective on $u$. Then there exists a neighborhood $t$ of $s$ such that $f$ is injective on $t$.

Set.InjOn.exists_isOpen_superset theorem

 {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} {s : Set X} (inj : InjOn f s)
  (sc : IsCompact s) (fc : ∀ x ∈ s, ContinuousAt f x) (loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u) :
  ∃ t, IsOpen t ∧ s ⊆ t ∧ InjOn f t

Full source

/-- If a function `f` is

- injective on a compact set `s`;
- continuous at every point of this set;
- injective on a neighborhood of each point of this set,

then it is injective on an open neighborhood of this set. -/
theorem Set.InjOn.exists_isOpen_superset {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    [T2Space Y] {f : X → Y} {s : Set X} (inj : InjOn f s) (sc : IsCompact s)
    (fc : ∀ x ∈ s, ContinuousAt f x) (loc : ∀ x ∈ s, ∃ u ∈ 𝓝 x, InjOn f u) :
    ∃ t, IsOpen t ∧ s ⊆ t ∧ InjOn f t :=
  let ⟨_t, hst, ht⟩ := inj.exists_mem_nhdsSet sc fc loc
  let ⟨u, huo, hsu, hut⟩ := mem_nhdsSet_iff_exists.1 hst
  ⟨u, huo, hsu, ht.mono hut⟩

Existence of Open Neighborhood Preserving Injectivity for Functions on Compact Sets in Hausdorff Spaces

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ Hausdorff, and let $f : X \to Y$ be a function. Suppose that: 1. $f$ is injective on a compact subset $s \subseteq X$; 2. $f$ is continuous at every point of $s$; 3. For each $x \in s$, there exists a neighborhood $u$ of $x$ such that $f$ is injective on $u$. Then there exists an open neighborhood $t$ of $s$ such that $f$ is injective on $t$.

lim_eq theorem

{x : X} [NeBot f] (h : f ≤ 𝓝 x) : @lim _ _ ⟨x⟩ f = x

Full source

theorem lim_eq {x : X} [NeBot f] (h : f ≤ 𝓝 x) : @lim _ _ ⟨x⟩ f = x :=
  tendsto_nhds_unique (le_nhds_lim ⟨x, h⟩) h

Limit Characterization in Hausdorff Spaces: $\lim f = x$ when $f$ converges to $x$

Informal description

Let $X$ be a Hausdorff space, $f$ a filter on $X$ that is not the trivial filter, and $x \in X$. If $f$ converges to $x$ (i.e., $f$ is finer than the neighborhood filter of $x$), then the limit of $f$ is equal to $x$.

lim_eq_iff theorem

[NeBot f] (h : ∃ x : X, f ≤ 𝓝 x) {x} : @lim _ _ ⟨x⟩ f = x ↔ f ≤ 𝓝 x

Full source

theorem lim_eq_iff [NeBot f] (h : ∃ x : X, f ≤ 𝓝 x) {x} : @lim _ _ ⟨x⟩ f = x ↔ f ≤ 𝓝 x :=
  ⟨fun c => c ▸ le_nhds_lim h, lim_eq⟩

Limit Characterization in Hausdorff Spaces: $\lim f = x$ if and only if $f$ converges to $x$

Informal description

Let $X$ be a Hausdorff space and $f$ a filter on $X$ that is not the trivial filter. Suppose there exists some $x \in X$ such that $f$ converges to $x$ (i.e., $f$ is finer than the neighborhood filter of $x$). Then for any $x \in X$, the limit of $f$ equals $x$ if and only if $f$ converges to $x$.

Ultrafilter.lim_eq_iff_le_nhds theorem

[CompactSpace X] {x : X} {F : Ultrafilter X} : F.lim = x ↔ ↑F ≤ 𝓝 x

Full source

theorem Ultrafilter.lim_eq_iff_le_nhds [CompactSpace X] {x : X} {F : Ultrafilter X} :
    F.lim = x ↔ ↑F ≤ 𝓝 x :=
  ⟨fun h => h ▸ F.le_nhds_lim, lim_eq⟩

Ultrafilter Limit Characterization in Compact Hausdorff Spaces: $F.\text{lim} = x \leftrightarrow F \leq \mathcal{N}(x)$

Informal description

Let $X$ be a compact Hausdorff space, $x \in X$, and $F$ an ultrafilter on $X$. Then the limit point of $F$ is equal to $x$ if and only if $F$ converges to $x$ (i.e., $F$ is finer than the neighborhood filter of $x$).

isOpen_iff_ultrafilter' theorem

[CompactSpace X] (U : Set X) : IsOpen U ↔ ∀ F : Ultrafilter X, F.lim ∈ U → U ∈ F.1

Full source

theorem isOpen_iff_ultrafilter' [CompactSpace X] (U : Set X) :
    IsOpenIsOpen U ↔ ∀ F : Ultrafilter X, F.lim ∈ U → U ∈ F.1 := by
  rw [isOpen_iff_ultrafilter]
  refine ⟨fun h F hF => h F.lim hF F F.le_nhds_lim, ?_⟩
  intro cond x hx f h
  rw [← Ultrafilter.lim_eq_iff_le_nhds.2 h] at hx
  exact cond _ hx

Characterization of Open Sets in Compact Hausdorff Spaces via Ultrafilter Limits

Informal description

Let $X$ be a compact Hausdorff space. A subset $U \subseteq X$ is open if and only if for every ultrafilter $F$ on $X$, whenever the limit point of $F$ belongs to $U$, then $U$ is an element of $F$.

Filter.Tendsto.limUnder_eq theorem

{x : X} {f : Filter Y} [NeBot f] {g : Y → X} (h : Tendsto g f (𝓝 x)) : @limUnder _ _ _ ⟨x⟩ f g = x

Full source

theorem Filter.Tendsto.limUnder_eq {x : X} {f : Filter Y} [NeBot f] {g : Y → X}
    (h : Tendsto g f (𝓝 x)) : @limUnder _ _ _ ⟨x⟩ f g = x :=
  lim_eq h

Limit Characterization under a Filter in Hausdorff Spaces: $\lim_{f} g = x$ when $g$ tends to $x$ along $f$

Informal description

Let $X$ be a Hausdorff space, $Y$ a topological space, $f$ a filter on $Y$ that is not the trivial filter, and $g : Y \to X$ a function. If $g$ tends to $x \in X$ along $f$ (i.e., the filter $g(f)$ is finer than the neighborhood filter of $x$), then the limit of $g$ along $f$ is equal to $x$.

Filter.limUnder_eq_iff theorem

 {f : Filter Y} [NeBot f] {g : Y → X} (h : ∃ x, Tendsto g f (𝓝 x)) {x} : @limUnder _ _ _ ⟨x⟩ f g = x ↔ Tendsto g f (𝓝 x)

Full source

theorem Filter.limUnder_eq_iff {f : Filter Y} [NeBot f] {g : Y → X} (h : ∃ x, Tendsto g f (𝓝 x))
    {x} : @limUnder _ _ _ ⟨x⟩ f g = x ↔ Tendsto g f (𝓝 x) :=
  ⟨fun c => c ▸ tendsto_nhds_limUnder h, Filter.Tendsto.limUnder_eq⟩

Limit Characterization under a Filter in Hausdorff Spaces: $\lim_{f} g = x$ if and only if $g$ tends to $x$ along $f$

Informal description

Let $X$ be a Hausdorff space, $Y$ a topological space, $f$ a filter on $Y$ that is not the trivial filter, and $g : Y \to X$ a function. Suppose there exists some $x \in X$ such that $g$ tends to $x$ along $f$ (i.e., the filter $g(f)$ is finer than the neighborhood filter of $x$). Then for any $x \in X$, the limit of $g$ along $f$ equals $x$ if and only if $g$ tends to $x$ along $f$.

Continuous.limUnder_eq theorem

[TopologicalSpace Y] {f : Y → X} (h : Continuous f) (y : Y) : @limUnder _ _ _ ⟨f y⟩ (𝓝 y) f = f y

Full source

theorem Continuous.limUnder_eq [TopologicalSpace Y] {f : Y → X} (h : Continuous f) (y : Y) :
    @limUnder _ _ _ ⟨f y⟩ (𝓝 y) f = f y :=
  (h.tendsto y).limUnder_eq

Limit of Continuous Function at a Point Equals its Value

Informal description

Let $X$ be a Hausdorff space and $Y$ a topological space. For any continuous function $f : Y \to X$ and any point $y \in Y$, the limit of $f$ along the neighborhood filter of $y$ is equal to $f(y)$, i.e., $\lim_{x \to y} f(x) = f(y)$.

lim_nhds theorem

(x : X) : @lim _ _ ⟨x⟩ (𝓝 x) = x

Full source

@[simp]
theorem lim_nhds (x : X) : @lim _ _ ⟨x⟩ (𝓝 x) = x :=
  lim_eq le_rfl

Limit of Neighborhood Filter in Hausdorff Space is the Point Itself

Informal description

For any point $x$ in a Hausdorff space $X$, the limit of the neighborhood filter $\mathcal{N}_x$ is equal to $x$ itself, i.e., $\lim \mathcal{N}_x = x$.

limUnder_nhds_id theorem

(x : X) : @limUnder _ _ _ ⟨x⟩ (𝓝 x) id = x

Full source

@[simp]
theorem limUnder_nhds_id (x : X) : @limUnder _ _ _ ⟨x⟩ (𝓝 x) id = x :=
  lim_nhds x

Limit of Identity Function Under Neighborhood Filter in Hausdorff Space

Informal description

For any point $x$ in a Hausdorff space $X$, the limit of the identity function under the neighborhood filter $\mathcal{N}_x$ is equal to $x$ itself, i.e., $\lim_{y \to x} y = x$.

lim_nhdsWithin theorem

{x : X} {s : Set X} (h : x ∈ closure s) : @lim _ _ ⟨x⟩ (𝓝[s] x) = x

Full source

@[simp]
theorem lim_nhdsWithin {x : X} {s : Set X} (h : x ∈ closure s) : @lim _ _ ⟨x⟩ (𝓝[s] x) = x :=
  haveI : NeBot (𝓝[s] x) := mem_closure_iff_clusterPt.1 h
  lim_eq inf_le_left

Limit Characterization in Hausdorff Spaces: $\lim (\mathcal{N}_s(x)) = x$ for $x \in \overline{s}$

Informal description

Let $X$ be a Hausdorff space, $x \in X$, and $s \subseteq X$ such that $x$ is in the closure of $s$. Then the limit of the neighborhood filter of $x$ restricted to $s$ is equal to $x$, i.e., $\lim (\mathcal{N}_s(x)) = x$.

limUnder_nhdsWithin_id theorem

{x : X} {s : Set X} (h : x ∈ closure s) : @limUnder _ _ _ ⟨x⟩ (𝓝[s] x) id = x

Full source

@[simp]
theorem limUnder_nhdsWithin_id {x : X} {s : Set X} (h : x ∈ closure s) :
    @limUnder _ _ _ ⟨x⟩ (𝓝[s] x) id = x :=
  lim_nhdsWithin h

Limit of Identity Function in Neighborhood Filter Restricted to Set Closure

Informal description

Let $X$ be a Hausdorff space, $x \in X$, and $s \subseteq X$ such that $x$ is in the closure of $s$. Then the limit of the identity function under the neighborhood filter of $x$ restricted to $s$ is equal to $x$, i.e., $\lim_{y \to x, y \in s} y = x$.

DiscreteTopology.toT2Space instance

[DiscreteTopology X] : T2Space X

Full source

instance (priority := 100) DiscreteTopology.toT2Space
    [DiscreteTopology X] : T2Space X :=
  ⟨fun x y h => ⟨{x}, {y}, isOpen_discrete _, isOpen_discrete _, rfl, rfl, disjoint_singleton.2 h⟩⟩

Discrete Spaces are Hausdorff

Informal description

Every discrete topological space is a Hausdorff space.

separated_by_continuous theorem

 [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) {x y : X} (h : f x ≠ f y) :
  ∃ u v : Set X, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v

Full source

theorem separated_by_continuous [TopologicalSpace Y] [T2Space Y]
    {f : X → Y} (hf : Continuous f) {x y : X} (h : f x ≠ f y) :
    ∃ u v : Set X, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ Disjoint u v :=
  let ⟨u, v, uo, vo, xu, yv, uv⟩ := t2_separation h
  ⟨f ⁻¹' u, f ⁻¹' v, uo.preimage hf, vo.preimage hf, xu, yv, uv.preimage _⟩

Continuous Maps Preserve Separation in Hausdorff Codomain

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ Hausdorff, and let $f : X \to Y$ be a continuous map. For any two points $x, y \in X$ such that $f(x) \neq f(y)$, there exist disjoint open sets $U, V \subseteq X$ with $x \in U$, $y \in V$, and $U \cap V = \emptyset$.

separated_by_isOpenEmbedding theorem

 [TopologicalSpace Y] [T2Space X] {f : X → Y} (hf : IsOpenEmbedding f) {x y : X} (h : x ≠ y) :
  ∃ u v : Set Y, IsOpen u ∧ IsOpen v ∧ f x ∈ u ∧ f y ∈ v ∧ Disjoint u v

Full source

theorem separated_by_isOpenEmbedding [TopologicalSpace Y] [T2Space X]
    {f : X → Y} (hf : IsOpenEmbedding f) {x y : X} (h : x ≠ y) :
    ∃ u v : Set Y, IsOpen u ∧ IsOpen v ∧ f x ∈ u ∧ f y ∈ v ∧ Disjoint u v :=
  let ⟨u, v, uo, vo, xu, yv, uv⟩ := t2_separation h
  ⟨f '' u, f '' v, hf.isOpenMap _ uo, hf.isOpenMap _ vo, mem_image_of_mem _ xu,
    mem_image_of_mem _ yv, disjoint_image_of_injective hf.injective uv⟩

Open Embeddings Preserve Hausdorff Separation

Informal description

Let $X$ be a Hausdorff space and $Y$ a topological space. Given an open embedding $f : X \to Y$ and two distinct points $x, y \in X$, there exist disjoint open sets $U, V \subseteq Y$ such that $f(x) \in U$ and $f(y) \in V$.

instT2SpaceSubtype instance

{p : X → Prop} [T2Space X] : T2Space (Subtype p)

Full source

instance {p : X → Prop} [T2Space X] : T2Space (Subtype p) := inferInstance

Subspaces of Hausdorff Spaces are Hausdorff

Informal description

For any topological space $X$ that is Hausdorff and any predicate $p$ on $X$, the subtype $\{x \in X \mid p(x)\}$ is also a Hausdorff space when equipped with the subspace topology.

Prod.t2Space instance

[T2Space X] [TopologicalSpace Y] [T2Space Y] : T2Space (X × Y)

Full source

instance Prod.t2Space [T2Space X] [TopologicalSpace Y] [T2Space Y] : T2Space (X × Y) :=
  inferInstance

Product of Hausdorff Spaces is Hausdorff

Informal description

The product $X \times Y$ of two Hausdorff spaces $X$ and $Y$ is also a Hausdorff space.

T2Space.of_injective_continuous theorem

[TopologicalSpace Y] [T2Space Y] {f : X → Y} (hinj : Injective f) (hc : Continuous f) : T2Space X

Full source

/-- If the codomain of an injective continuous function is a Hausdorff space, then so is its
domain. -/
theorem T2Space.of_injective_continuous [TopologicalSpace Y] [T2Space Y] {f : X → Y}
    (hinj : Injective f) (hc : Continuous f) : T2Space X :=
  ⟨fun _ _ h => separated_by_continuous hc (hinj.ne h)⟩

Hausdorff Property via Injective Continuous Map

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ Hausdorff. If there exists an injective continuous map $f : X \to Y$, then $X$ is also a Hausdorff space.

Topology.IsEmbedding.t2Space theorem

[TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : IsEmbedding f) : T2Space X

Full source

/-- If the codomain of a topological embedding is a Hausdorff space, then so is its domain.
See also `T2Space.of_continuous_injective`. -/
theorem Topology.IsEmbedding.t2Space [TopologicalSpace Y] [T2Space Y] {f : X → Y}
    (hf : IsEmbedding f) : T2Space X :=
  .of_injective_continuous hf.injective hf.continuous

Hausdorff Property via Topological Embedding

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ Hausdorff. If $f : X \to Y$ is a topological embedding, then $X$ is also a Hausdorff space.

Homeomorph.t2Space theorem

[TopologicalSpace Y] [T2Space X] (h : X ≃ₜ Y) : T2Space Y

Full source

protected theorem Homeomorph.t2Space [TopologicalSpace Y] [T2Space X] (h : X ≃ₜ Y) : T2Space Y :=
  h.symm.isEmbedding.t2Space

Hausdorff Property Preserved under Homeomorphism

Informal description

Let $X$ and $Y$ be topological spaces, with $X$ being Hausdorff. If there exists a homeomorphism $h: X \simeq Y$, then $Y$ is also a Hausdorff space.

ULift.instT2Space instance

[T2Space X] : T2Space (ULift X)

Full source

instance ULift.instT2Space [T2Space X] : T2Space (ULift X) :=
  IsEmbedding.uliftDown.t2Space

Lifted Hausdorff Space is Hausdorff

Informal description

For any Hausdorff space $X$, the lifted space $\text{ULift}\, X$ is also a Hausdorff space.

instT2SpaceSum instance

[T2Space X] [TopologicalSpace Y] [T2Space Y] : T2Space (X ⊕ Y)

Full source

instance [T2Space X] [TopologicalSpace Y] [T2Space Y] :
    T2Space (X ⊕ Y) := by
  constructor
  rintro (x | x) (y | y) h
  · exact separated_by_isOpenEmbedding .inl <| ne_of_apply_ne _ h
  · exact separated_by_continuous continuous_isLeft <| by simp
  · exact separated_by_continuous continuous_isLeft <| by simp
  · exact separated_by_isOpenEmbedding .inr <| ne_of_apply_ne _ h

Direct Sum of Hausdorff Spaces is Hausdorff

Informal description

For any two Hausdorff spaces $X$ and $Y$, their direct sum $X \oplus Y$ is also a Hausdorff space.

Pi.t2Space instance

{Y : X → Type v} [∀ a, TopologicalSpace (Y a)] [∀ a, T2Space (Y a)] : T2Space (∀ a, Y a)

Full source

instance Pi.t2Space {Y : X → Type v} [∀ a, TopologicalSpace (Y a)]
    [∀ a, T2Space (Y a)] : T2Space (∀ a, Y a) :=
  inferInstance

Product of Hausdorff Spaces is Hausdorff

Informal description

For any family of topological spaces $\{Y_a\}_{a \in X}$ where each $Y_a$ is a Hausdorff space, the product space $\prod_{a \in X} Y_a$ is also a Hausdorff space.

Sigma.t2Space instance

{ι} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ a, T2Space (X a)] : T2Space (Σ i, X i)

Full source

instance Sigma.t2Space {ι} {X : ι → Type*} [∀ i, TopologicalSpace (X i)] [∀ a, T2Space (X a)] :
    T2Space (Σi, X i) := by
  constructor
  rintro ⟨i, x⟩ ⟨j, y⟩ neq
  rcases eq_or_ne i j with (rfl | h)
  · replace neq : x ≠ y := ne_of_apply_ne _ neq
    exact separated_by_isOpenEmbedding .sigmaMk neq
  · let _ := (⊥ : TopologicalSpace ι); have : DiscreteTopology ι := ⟨rfl⟩
    exact separated_by_continuous (continuous_def.2 fun u _ => isOpen_sigma_fst_preimage u) h

Disjoint Union of Hausdorff Spaces is Hausdorff

Informal description

For any family of topological spaces $\{X_i\}_{i \in \iota}$ where each $X_i$ is a Hausdorff space, the disjoint union $\Sigma i, X_i$ is also a Hausdorff space.

t2Setoid definition

: Setoid X

Full source

/-- The smallest equivalence relation on a topological space giving a T2 quotient. -/
def t2Setoid : Setoid X := sInf {s | T2Space (Quotient s)}

Hausdorff quotient equivalence relation

Informal description

The smallest equivalence relation on a topological space $ X $ such that the quotient space is Hausdorff (T₂). This equivalence relation is defined as the infimum of all equivalence relations $ s $ on $ X $ for which the quotient space $ \text{Quotient } s $ is Hausdorff.

t2Quotient definition

Full source

/-- The largest T2 quotient of a topological space. This construction is left-adjoint to the
inclusion of T2 spaces into all topological spaces. -/
def t2Quotient := Quotient (t2Setoid X)

Largest Hausdorff quotient of a topological space

Informal description

The largest Hausdorff quotient of a topological space $ X $, constructed as the quotient space of $ X $ by the equivalence relation `t2Setoid X`. This construction is the left adjoint to the inclusion of Hausdorff spaces into all topological spaces.

t2Quotient.instTopologicalSpace instance

: TopologicalSpace (t2Quotient X)

Full source

instance : TopologicalSpace (t2Quotient X) :=
  inferInstanceAs <| TopologicalSpace (Quotient _)

Topology on the Largest Hausdorff Quotient

Informal description

The largest Hausdorff quotient $\text{t2Quotient } X$ of a topological space $X$ is equipped with the quotient topology induced by the canonical projection map from $X$ to $\text{t2Quotient } X$.

t2Quotient.mk definition

: X → t2Quotient X

Full source

/-- The map from a topological space to its largest T2 quotient. -/
def mk : X → t2Quotient X := Quotient.mk (t2Setoid X)

Projection to the largest Hausdorff quotient

Informal description

The canonical projection map from a topological space $ X $ to its largest Hausdorff quotient $ \text{t2Quotient } X $, which sends each point $ x \in X $ to its equivalence class under the relation `t2Setoid X`.

t2Quotient.mk_eq theorem

{x y : X} : mk x = mk y ↔ ∀ s : Setoid X, T2Space (Quotient s) → s x y

Full source

lemma mk_eq {x y : X} : mkmk x = mk y ↔ ∀ s : Setoid X, T2Space (Quotient s) → s x y :=
  Setoid.quotient_mk_sInf_eq

Equality in Largest Hausdorff Quotient via All Hausdorff-Compatible Equivalence Relations

Informal description

For any two points $x, y$ in a topological space $X$, the images of $x$ and $y$ under the projection map to the largest Hausdorff quotient $\text{t2Quotient } X$ are equal if and only if $x$ and $y$ are related by every equivalence relation $s$ on $X$ for which the quotient space $\text{Quotient } s$ is Hausdorff. In other words, \[ \text{mk}(x) = \text{mk}(y) \leftrightarrow \forall s \text{ (Setoid on } X), \text{Quotient } s \text{ is T₂} \implies s(x, y). \]

t2Quotient.surjective_mk theorem

: Surjective (mk : X → t2Quotient X)

Full source

lemma surjective_mk : Surjective (mk : X → t2Quotient X) := Quotient.mk_surjective

Surjectivity of the Projection to the Largest Hausdorff Quotient

Informal description

The canonical projection map $\text{mk} \colon X \to \text{t2Quotient}\, X$ from a topological space $X$ to its largest Hausdorff quotient is surjective. That is, for every element $q$ in $\text{t2Quotient}\, X$, there exists a point $x \in X$ such that $\text{mk}(x) = q$.

t2Quotient.continuous_mk theorem

: Continuous (mk : X → t2Quotient X)

Full source

lemma continuous_mk : Continuous (mk : X → t2Quotient X) :=
  continuous_quotient_mk'

Continuity of the Projection to the Largest Hausdorff Quotient

Informal description

The canonical projection map $\text{mk} \colon X \to \text{t2Quotient } X$ from a topological space $X$ to its largest Hausdorff quotient is continuous.

t2Quotient.inductionOn theorem

{motive : t2Quotient X → Prop} (q : t2Quotient X) (h : ∀ x, motive (t2Quotient.mk x)) : motive q

Full source

@[elab_as_elim]
protected lemma inductionOn {motive : t2Quotient X → Prop} (q : t2Quotient X)
    (h : ∀ x, motive (t2Quotient.mk x)) : motive q := Quotient.inductionOn q h

Induction Principle for the Largest Hausdorff Quotient

Informal description

Let $X$ be a topological space and let $\text{t2Quotient}\, X$ be its largest Hausdorff quotient. For any predicate $\text{motive}$ on $\text{t2Quotient}\, X$ and any element $q \in \text{t2Quotient}\, X$, if $\text{motive}$ holds for the image of every point $x \in X$ under the canonical projection $\text{mk} : X \to \text{t2Quotient}\, X$, then $\text{motive}$ holds for $q$.

t2Quotient.inductionOn₂ theorem

 [TopologicalSpace Y] {motive : t2Quotient X → t2Quotient Y → Prop} (q : t2Quotient X) (q' : t2Quotient Y)
  (h : ∀ x y, motive (mk x) (mk y)) : motive q q'

Full source

@[elab_as_elim]
protected lemma inductionOn₂ [TopologicalSpace Y] {motive : t2Quotient X → t2Quotient Y → Prop}
    (q : t2Quotient X) (q' : t2Quotient Y) (h : ∀ x y, motive (mk x) (mk y)) : motive q q' :=
  Quotient.inductionOn₂ q q' h

Double Induction Principle for Largest Hausdorff Quotients

Informal description

Let $X$ and $Y$ be topological spaces, and let $\text{t2Quotient}\, X$ and $\text{t2Quotient}\, Y$ be their largest Hausdorff quotients. For any predicate $\text{motive}$ on $\text{t2Quotient}\, X \times \text{t2Quotient}\, Y$ and any elements $q \in \text{t2Quotient}\, X$ and $q' \in \text{t2Quotient}\, Y$, if $\text{motive}$ holds for the pair $(\text{mk}\, x, \text{mk}\, y)$ for all $x \in X$ and $y \in Y$, then $\text{motive}$ holds for $(q, q')$.

t2Quotient.instT2Space instance

: T2Space (t2Quotient X)

Full source

/-- The largest T2 quotient of a topological space is indeed T2. -/
instance : T2Space (t2Quotient X) := by
  rw [t2Space_iff]
  rintro ⟨x⟩ ⟨y⟩ (h : ¬ t2Quotient.mk x = t2Quotient.mk y)
  obtain ⟨s, hs, hsxy⟩ : ∃ s, T2Space (Quotient s) ∧ Quotient.mk s x ≠ Quotient.mk s y := by
    simpa [t2Quotient.mk_eq] using h
  exact separated_by_continuous (continuous_map_sInf (by exact hs)) hsxy

The Largest Hausdorff Quotient is Hausdorff

Informal description

The largest Hausdorff quotient $\text{t2Quotient}\, X$ of a topological space $X$ is a Hausdorff space.

t2Quotient.compatible theorem

 {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) :
  letI _ := t2Setoid X
  ∀ (a b : X), a ≈ b → f a = f b

Full source

lemma compatible {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y]
    {f : X → Y} (hf : Continuous f) : letI _ := t2Setoid X
    ∀ (a b : X), a ≈ b → f a = f b := by
  change t2Setoid X ≤ Setoid.ker f
  exact sInf_le <| .of_injective_continuous
    (Setoid.ker_lift_injective _) (hf.quotient_lift fun _ _ ↦ id)

Compatibility of Continuous Functions with Hausdorff Quotient Relation

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ Hausdorff, and let $f: X \to Y$ be a continuous function. Then for any two points $a, b \in X$ that are equivalent under the Hausdorff quotient equivalence relation (i.e., $a \approx b$), we have $f(a) = f(b)$.

t2Quotient.lift definition

 {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) : t2Quotient X → Y

Full source

/-- The universal property of the largest T2 quotient of a topological space `X`: any continuous
map from `X` to a T2 space `Y` uniquely factors through `t2Quotient X`. This declaration builds the
factored map. Its continuity is `t2Quotient.continuous_lift`, the fact that it indeed factors the
original map is `t2Quotient.lift_mk` and uniqueness is `t2Quotient.unique_lift`. -/
def lift {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y]
    {f : X → Y} (hf : Continuous f) : t2Quotient X → Y :=
  Quotient.lift f (t2Quotient.compatible hf)

Factorization of continuous maps through the largest Hausdorff quotient

Informal description

Given a continuous map $ f : X \to Y $ from a topological space $ X $ to a Hausdorff space $ Y $, the function `t2Quotient.lift hf` is the unique continuous map from the largest Hausdorff quotient `t2Quotient X` to $ Y $ that factors $ f $ through the quotient map $ X \to \text{t2Quotient}\, X $. Specifically, for any $ x \in X $, we have $ \text{lift}\, hf\, (\text{mk}\, x) = f x $, where `mk` is the quotient map.

t2Quotient.continuous_lift theorem

 {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) :
  Continuous (t2Quotient.lift hf)

Full source

lemma continuous_lift {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y]
    {f : X → Y} (hf : Continuous f) : Continuous (t2Quotient.lift hf) :=
  continuous_coinduced_dom.mpr hf

Continuity of the lift through the largest Hausdorff quotient

Informal description

Given a continuous map $f \colon X \to Y$ from a topological space $X$ to a Hausdorff space $Y$, the induced map $\text{t2Quotient.lift}\, hf \colon \text{t2Quotient}\, X \to Y$ is continuous.

t2Quotient.lift_mk theorem

 {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f) (x : X) :
  lift hf (mk x) = f x

Full source

@[simp]
lemma lift_mk {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y]
    {f : X → Y} (hf : Continuous f) (x : X) : lift hf (mk x) = f x :=
  Quotient.lift_mk (s := t2Setoid X) f (t2Quotient.compatible hf) x

Factorization Property of Continuous Maps through Hausdorff Quotient

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ Hausdorff, and let $f : X \to Y$ be a continuous function. Then for any point $x \in X$, the lift of $f$ to the largest Hausdorff quotient of $X$ evaluated at the image of $x$ under the quotient map equals $f(x)$, i.e., $\text{lift}\, hf\, (\text{mk}\, x) = f x$.

t2Quotient.unique_lift theorem

 {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y] {f : X → Y} (hf : Continuous f)
  {g : t2Quotient X → Y} (hfg : g ∘ mk = f) : g = lift hf

Full source

lemma unique_lift {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T2Space Y]
    {f : X → Y} (hf : Continuous f) {g : t2Quotient X → Y} (hfg : g ∘ mk = f) :
    g = lift hf := by
  apply surjective_mk X |>.right_cancellable |>.mp <| funext _
  simp [← hfg]

Uniqueness of Continuous Lift Through Largest Hausdorff Quotient

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ Hausdorff, and let $f : X \to Y$ be a continuous map. For any continuous map $g : \text{t2Quotient}\, X \to Y$ satisfying $g \circ \text{mk} = f$, we have $g = \text{lift}\, hf$, where $\text{mk} : X \to \text{t2Quotient}\, X$ is the canonical projection and $\text{lift}\, hf$ is the unique factorization of $f$ through the largest Hausdorff quotient.

isClosed_eq theorem

[T2Space X] {f g : Y → X} (hf : Continuous f) (hg : Continuous g) : IsClosed {y : Y | f y = g y}

Full source

theorem isClosed_eq [T2Space X] {f g : Y → X} (hf : Continuous f) (hg : Continuous g) :
    IsClosed { y : Y | f y = g y } :=
  continuous_iff_isClosed.mp (hf.prodMk hg) _ isClosed_diagonal

Closedness of Equalizer Set for Continuous Functions in Hausdorff Space

Informal description

Let $X$ be a Hausdorff space and $Y$ a topological space. For any two continuous functions $f, g : Y \to X$, the set $\{y \in Y \mid f(y) = g(y)\}$ is closed in $Y$.

IsClosed.isClosed_eq theorem

 [T2Space Y] {f g : X → Y} {s : Set X} (hs : IsClosed s) (hf : ContinuousOn f s) (hg : ContinuousOn g s) :
  IsClosed ({x ∈ s | f x = g x})

Full source

/-- If functions `f` and `g` are continuous on a closed set `s`,
then the set of points `x ∈ s` such that `f x = g x` is a closed set. -/
protected theorem IsClosed.isClosed_eq [T2Space Y] {f g : X → Y} {s : Set X} (hs : IsClosed s)
    (hf : ContinuousOn f s) (hg : ContinuousOn g s) : IsClosed {x ∈ s | f x = g x} :=
  (hf.prodMk hg).preimage_isClosed_of_isClosed hs isClosed_diagonal

Closedness of Equalizer Set for Continuous Functions on a Closed Subset in Hausdorff Space

Informal description

Let $Y$ be a Hausdorff space, $X$ a topological space, and $s$ a closed subset of $X$. If $f, g : X \to Y$ are continuous on $s$, then the set $\{x \in s \mid f(x) = g(x)\}$ is closed in $X$.

isOpen_ne_fun theorem

[T2Space X] {f g : Y → X} (hf : Continuous f) (hg : Continuous g) : IsOpen {y : Y | f y ≠ g y}

Full source

theorem isOpen_ne_fun [T2Space X] {f g : Y → X} (hf : Continuous f) (hg : Continuous g) :
    IsOpen { y : Y | f y ≠ g y } :=
  isOpen_compl_iff.mpr <| isClosed_eq hf hg

Openness of Non-Equalizer Set for Continuous Functions in Hausdorff Space

Informal description

Let $X$ be a Hausdorff space and $Y$ a topological space. For any two continuous functions $f, g : Y \to X$, the set $\{y \in Y \mid f(y) \neq g(y)\}$ is open in $Y$.

Set.EqOn.closure theorem

[T2Space X] {s : Set Y} {f g : Y → X} (h : EqOn f g s) (hf : Continuous f) (hg : Continuous g) : EqOn f g (closure s)

Full source

/-- If two continuous maps are equal on `s`, then they are equal on the closure of `s`. See also
`Set.EqOn.of_subset_closure` for a more general version. -/
protected theorem Set.EqOn.closure [T2Space X] {s : Set Y} {f g : Y → X} (h : EqOn f g s)
    (hf : Continuous f) (hg : Continuous g) : EqOn f g (closure s) :=
  closure_minimal h (isClosed_eq hf hg)

Continuous Functions Equal on a Set are Equal on its Closure in Hausdorff Space

Informal description

Let $X$ be a Hausdorff space and $Y$ a topological space. If two continuous functions $f, g : Y \to X$ are equal on a subset $s \subseteq Y$, then they are also equal on the closure of $s$.

Continuous.ext_on theorem

[T2Space X] {s : Set Y} (hs : Dense s) {f g : Y → X} (hf : Continuous f) (hg : Continuous g) (h : EqOn f g s) : f = g

Full source

/-- If two continuous functions are equal on a dense set, then they are equal. -/
theorem Continuous.ext_on [T2Space X] {s : Set Y} (hs : Dense s) {f g : Y → X} (hf : Continuous f)
    (hg : Continuous g) (h : EqOn f g s) : f = g :=
  funext fun x => h.closure hf hg (hs x)

Uniqueness of Continuous Functions on Hausdorff Spaces via Dense Sets

Informal description

Let $X$ be a Hausdorff space and $Y$ a topological space. If two continuous functions $f, g : Y \to X$ are equal on a dense subset $s \subseteq Y$, then $f = g$ on the whole space $Y$.

eqOn_closure₂' theorem

 [T2Space Z] {s : Set X} {t : Set Y} {f g : X → Y → Z} (h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y)
  (hf₁ : ∀ x, Continuous (f x)) (hf₂ : ∀ y, Continuous fun x => f x y) (hg₁ : ∀ x, Continuous (g x))
  (hg₂ : ∀ y, Continuous fun x => g x y) : ∀ x ∈ closure s, ∀ y ∈ closure t, f x y = g x y

Full source

theorem eqOn_closure₂' [T2Space Z] {s : Set X} {t : Set Y} {f g : X → Y → Z}
    (h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y) (hf₁ : ∀ x, Continuous (f x))
    (hf₂ : ∀ y, Continuous fun x => f x y) (hg₁ : ∀ x, Continuous (g x))
    (hg₂ : ∀ y, Continuous fun x => g x y) : ∀ x ∈ closure s, ∀ y ∈ closure t, f x y = g x y :=
  suffices closureclosure s ⊆ ⋂ y ∈ closure t, { x | f x y = g x y } by simpa only [subset_def, mem_iInter]
  (closure_minimal fun x hx => mem_iInter₂.2 <| Set.EqOn.closure (h x hx) (hf₁ _) (hg₁ _)) <|
    isClosed_biInter fun _ _ => isClosed_eq (hf₂ _) (hg₂ _)

Equality of Continuous Functions on Product Space via Dense Subsets in Hausdorff Space

Informal description

Let $Z$ be a Hausdorff space, and let $s \subseteq X$, $t \subseteq Y$ be subsets. For two functions $f, g \colon X \times Y \to Z$ such that: 1. $f(x,y) = g(x,y)$ for all $x \in s$ and $y \in t$, 2. For each fixed $x$, the function $f(x,\cdot)$ is continuous, 3. For each fixed $y$, the function $f(\cdot,y)$ is continuous, 4. For each fixed $x$, the function $g(x,\cdot)$ is continuous, 5. For each fixed $y$, the function $g(\cdot,y)$ is continuous, then $f(x,y) = g(x,y)$ holds for all $x$ in the closure of $s$ and all $y$ in the closure of $t$.

eqOn_closure₂ theorem

 [T2Space Z] {s : Set X} {t : Set Y} {f g : X → Y → Z} (h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y)
  (hf : Continuous (uncurry f)) (hg : Continuous (uncurry g)) : ∀ x ∈ closure s, ∀ y ∈ closure t, f x y = g x y

Full source

theorem eqOn_closure₂ [T2Space Z] {s : Set X} {t : Set Y} {f g : X → Y → Z}
    (h : ∀ x ∈ s, ∀ y ∈ t, f x y = g x y) (hf : Continuous (uncurry f))
    (hg : Continuous (uncurry g)) : ∀ x ∈ closure s, ∀ y ∈ closure t, f x y = g x y :=
  eqOn_closure₂' h hf.uncurry_left hf.uncurry_right hg.uncurry_left hg.uncurry_right

Continuous Functions Agree on Product of Closures in Hausdorff Space

Informal description

Let $Z$ be a Hausdorff space, $X$ and $Y$ topological spaces, and $s \subseteq X$, $t \subseteq Y$ subsets. For two continuous functions $f, g \colon X \times Y \to Z$ that agree on $s \times t$ (i.e., $f(x,y) = g(x,y)$ for all $x \in s$ and $y \in t$), then $f$ and $g$ also agree on $\overline{s} \times \overline{t}$ (i.e., $f(x,y) = g(x,y)$ for all $x \in \overline{s}$ and $y \in \overline{t}$).

Set.EqOn.of_subset_closure theorem

 [T2Space Y] {s t : Set X} {f g : X → Y} (h : EqOn f g s) (hf : ContinuousOn f t) (hg : ContinuousOn g t) (hst : s ⊆ t)
  (hts : t ⊆ closure s) : EqOn f g t

Full source

/-- If `f x = g x` for all `x ∈ s` and `f`, `g` are continuous on `t`, `s ⊆ t ⊆ closure s`, then
`f x = g x` for all `x ∈ t`. See also `Set.EqOn.closure`. -/
theorem Set.EqOn.of_subset_closure [T2Space Y] {s t : Set X} {f g : X → Y} (h : EqOn f g s)
    (hf : ContinuousOn f t) (hg : ContinuousOn g t) (hst : s ⊆ t) (hts : t ⊆ closure s) :
    EqOn f g t := by
  intro x hx
  have : (𝓝[s] x).NeBot := mem_closure_iff_clusterPt.mp (hts hx)
  exact
    tendsto_nhds_unique_of_eventuallyEq ((hf x hx).mono_left <| nhdsWithin_mono _ hst)
      ((hg x hx).mono_left <| nhdsWithin_mono _ hst) (h.eventuallyEq_of_mem self_mem_nhdsWithin)

Equality of Continuous Functions on Intermediate Set via Dense Subset in Hausdorff Space

Informal description

Let $Y$ be a Hausdorff space, $X$ a topological space, and $s, t \subseteq X$ subsets with $s \subseteq t \subseteq \overline{s}$. If two functions $f, g \colon X \to Y$ satisfy: 1. $f(x) = g(x)$ for all $x \in s$, 2. $f$ is continuous on $t$, 3. $g$ is continuous on $t$, then $f(x) = g(x)$ for all $x \in t$.

Function.LeftInverse.isClosed_range theorem

 [T2Space X] {f : X → Y} {g : Y → X} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) :
  IsClosed (range g)

Full source

theorem Function.LeftInverse.isClosed_range [T2Space X] {f : X → Y} {g : Y → X}
    (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) : IsClosed (range g) :=
  have : EqOn (g ∘ f) id (closure <| range g) :=
    h.rightInvOn_range.eqOn.closure (hg.comp hf) continuous_id
  isClosed_of_closure_subset fun x hx => ⟨f x, this hx⟩

Range of a Continuous Left Inverse is Closed in Hausdorff Space

Informal description

Let $X$ be a Hausdorff space and $Y$ a topological space. If $f : X \to Y$ and $g : Y \to X$ are continuous functions such that $f$ is a left inverse of $g$ (i.e., $f(g(y)) = y$ for all $y \in Y$), then the range of $g$ is a closed subset of $X$.

Function.LeftInverse.isClosedEmbedding theorem

 [T2Space X] {f : X → Y} {g : Y → X} (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) :
  IsClosedEmbedding g

Full source

theorem Function.LeftInverse.isClosedEmbedding [T2Space X] {f : X → Y} {g : Y → X}
    (h : Function.LeftInverse f g) (hf : Continuous f) (hg : Continuous g) : IsClosedEmbedding g :=
  ⟨.of_leftInverse h hf hg, h.isClosed_range hf hg⟩

Continuous Left Inverse Implies Closed Embedding in Hausdorff Space

Informal description

Let $X$ be a Hausdorff space and $Y$ a topological space. If $f : X \to Y$ and $g : Y \to X$ are continuous functions such that $f$ is a left inverse of $g$ (i.e., $f(g(y)) = y$ for all $y \in Y$), then $g$ is a closed embedding.

SeparatedNhds.of_isCompact_isCompact theorem

[T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) (hst : Disjoint s t) : SeparatedNhds s t

Full source

theorem SeparatedNhds.of_isCompact_isCompact [T2Space X] {s t : Set X} (hs : IsCompact s)
    (ht : IsCompact t) (hst : Disjoint s t) : SeparatedNhds s t := by
  simp only [SeparatedNhds, prod_subset_compl_diagonal_iff_disjoint.symm] at hst ⊢
  exact generalized_tube_lemma hs ht isClosed_diagonal.isOpen_compl hst

Separation of Disjoint Compact Sets in Hausdorff Space

Informal description

Let $X$ be a Hausdorff space, and let $s, t \subseteq X$ be two disjoint compact subsets. Then there exist disjoint open neighborhoods $U \supseteq s$ and $V \supseteq t$.

SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed theorem

 [T2Space X] {s : Set X} {t : Set X} (H1 : IsClosed s) (H2 : IsCompact (closure sᶜ)) (H3 : IsClosed t)
  (H4 : Disjoint s t) : SeparatedNhds s t

Full source

/-- In a `T2Space X`, for disjoint closed sets `s t` such that `closure sᶜ` is compact,
there are neighbourhoods that separate `s` and `t`. -/
lemma SeparatedNhds.of_isClosed_isCompact_closure_compl_isClosed [T2Space X] {s : Set X}
    {t : Set X} (H1 : IsClosed s) (H2 : IsCompact (closure sᶜ)) (H3 : IsClosed t)
    (H4 : Disjoint s t) : SeparatedNhds s t := by
  -- Since `t` is a closed subset of the compact set `closure sᶜ`, it is compact.
  have ht : IsCompact t := .of_isClosed_subset H2 H3 <| H4.subset_compl_left.trans subset_closure
  -- we split `s` into its frontier and its interior.
  rw [← diff_union_of_subset (interior_subset (s := s))]
  -- since `t ⊆ sᶜ`, which is open, and `interior s` is open, we have
  -- `SeparatedNhds (interior s) t`, which leaves us only with the frontier.
  refine .union_left ?_ ⟨interior s, sᶜ, isOpen_interior, H1.isOpen_compl, le_rfl,
    H4.subset_compl_left, disjoint_compl_right.mono_left interior_subset⟩
  -- Since the frontier of `s` is compact (as it is a subset of `closure sᶜ`), we simply apply
  -- `SeparatedNhds_of_isCompact_isCompact`.
  rw [← H1.frontier_eq, frontier_eq_closure_inter_closure, H1.closure_eq]
  refine .of_isCompact_isCompact ?_ ht (disjoint_of_subset_left inter_subset_left H4)
  exact H2.of_isClosed_subset (H1.inter isClosed_closure) inter_subset_right

Separation of Disjoint Closed Sets with Compact Complement Closure in Hausdorff Space

Informal description

Let $ X $ be a Hausdorff space, and let $ s, t \subseteq X $ be two disjoint closed sets. If the closure of the complement of $ s $ is compact, then there exist disjoint open neighborhoods $ U \supseteq s $ and $ V \supseteq t $.

SeparatedNhds.of_finset_finset theorem

[T2Space X] (s t : Finset X) (h : Disjoint s t) : SeparatedNhds (s : Set X) t

Full source

theorem SeparatedNhds.of_finset_finset [T2Space X] (s t : Finset X) (h : Disjoint s t) :
    SeparatedNhds (s : Set X) t :=
  .of_isCompact_isCompact s.finite_toSet.isCompact t.finite_toSet.isCompact <| mod_cast h

Separation of Disjoint Finite Sets in Hausdorff Space

Informal description

Let $X$ be a Hausdorff space, and let $s, t$ be two disjoint finite subsets of $X$. Then there exist disjoint open neighborhoods $U \supseteq s$ and $V \supseteq t$.

SeparatedNhds.of_singleton_finset theorem

[T2Space X] {x : X} {s : Finset X} (h : x ∉ s) : SeparatedNhds ({ x } : Set X) s

Full source

theorem SeparatedNhds.of_singleton_finset [T2Space X] {x : X} {s : Finset X} (h : x ∉ s) :
    SeparatedNhds ({x} : Set X) s :=
  mod_cast .of_finset_finset {x} s (Finset.disjoint_singleton_left.mpr h)

Separation of Point from Finite Set in Hausdorff Space

Informal description

Let $X$ be a Hausdorff space, $x \in X$ a point, and $s \subseteq X$ a finite subset such that $x \notin s$. Then there exist disjoint open sets $U$ and $V$ with $x \in U$ and $s \subseteq V$.

IsCompact.isClosed theorem

[T2Space X] {s : Set X} (hs : IsCompact s) : IsClosed s

Full source

/-- In a `T2Space`, every compact set is closed. -/
theorem IsCompact.isClosed [T2Space X] {s : Set X} (hs : IsCompact s) : IsClosed s :=
  isOpen_compl_iff.1 <| isOpen_iff_forall_mem_open.mpr fun x hx =>
    let ⟨u, v, _, vo, su, xv, uv⟩ :=
      SeparatedNhds.of_isCompact_isCompact hs isCompact_singleton (disjoint_singleton_right.2 hx)
    ⟨v, (uv.mono_left <| show s ≤ u from su).subset_compl_left, vo, by simpa using xv⟩

Compact Sets are Closed in Hausdorff Spaces

Informal description

In a Hausdorff space $X$, every compact subset $s \subseteq X$ is closed.

IsCompact.preimage_continuous theorem

[CompactSpace X] [T2Space Y] {f : X → Y} {s : Set Y} (hs : IsCompact s) (hf : Continuous f) : IsCompact (f ⁻¹' s)

Full source

theorem IsCompact.preimage_continuous [CompactSpace X] [T2Space Y] {f : X → Y} {s : Set Y}
    (hs : IsCompact s) (hf : Continuous f) : IsCompact (f ⁻¹' s) :=
  (hs.isClosed.preimage hf).isCompact

Compactness of Preimage under Continuous Map from Compact to Hausdorff Space

Informal description

Let $X$ be a compact space and $Y$ be a Hausdorff space. For any continuous function $f \colon X \to Y$ and any compact subset $s \subseteq Y$, the preimage $f^{-1}(s)$ is compact in $X$.

Pi.isCompact_iff theorem

 {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)] [∀ i, T2Space (π i)] {s : Set (Π i, π i)} :
  IsCompact s ↔ IsClosed s ∧ ∀ i, IsCompact (eval i '' s)

Full source

lemma Pi.isCompact_iff {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
    [∀ i, T2Space (π i)] {s : Set (Π i, π i)} :
    IsCompactIsCompact s ↔ IsClosed s ∧ ∀ i, IsCompact (eval i '' s) := by
  constructor <;> intro H
  · exact ⟨H.isClosed, fun i ↦ H.image <| continuous_apply i⟩
  · exact IsCompact.of_isClosed_subset (isCompact_univ_pi H.2) H.1 (subset_pi_eval_image univ s)

Compactness in Product of Hausdorff Spaces via Projections

Informal description

Let $\{\pi_i\}_{i \in \iota}$ be a family of topological spaces where each $\pi_i$ is a Hausdorff space, and let $s$ be a subset of the product space $\prod_{i \in \iota} \pi_i$. Then $s$ is compact if and only if $s$ is closed and for every index $i \in \iota$, the projection of $s$ onto $\pi_i$ is compact.

Pi.isCompact_closure_iff theorem

 {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)] [∀ i, T2Space (π i)] {s : Set (Π i, π i)} :
  IsCompact (closure s) ↔ ∀ i, IsCompact (closure <| eval i '' s)

Full source

lemma Pi.isCompact_closure_iff {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
    [∀ i, T2Space (π i)] {s : Set (Π i, π i)} :
    IsCompactIsCompact (closure s) ↔ ∀ i, IsCompact (closure <| eval i '' s) := by
  simp_rw [← exists_isCompact_superset_iff, Pi.exists_compact_superset_iff, image_subset_iff]

Compactness of Closure in Product of Hausdorff Spaces via Projections

Informal description

Let $\{π_i\}_{i \in \iota}$ be a family of topological spaces where each $π_i$ is a Hausdorff space, and let $s$ be a subset of the product space $\prod_{i \in \iota} π_i$. The closure of $s$ is compact if and only if for every index $i \in \iota$, the closure of the projection of $s$ onto $π_i$ is compact.

exists_subset_nhds_of_isCompact theorem

 [T2Space X] {ι : Type*} [Nonempty ι] {V : ι → Set X} (hV : Directed (· ⊇ ·) V) (hV_cpct : ∀ i, IsCompact (V i))
  {U : Set X} (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U

Full source

/-- If `V : ι → Set X` is a decreasing family of compact sets then any neighborhood of
`⋂ i, V i` contains some `V i`. This is a version of `exists_subset_nhds_of_isCompact'` where we
don't need to assume each `V i` closed because it follows from compactness since `X` is
assumed to be Hausdorff. -/
theorem exists_subset_nhds_of_isCompact [T2Space X] {ι : Type*} [Nonempty ι] {V : ι → Set X}
    (hV : Directed (· ⊇ ·) V) (hV_cpct : ∀ i, IsCompact (V i)) {U : Set X}
    (hU : ∀ x ∈ ⋂ i, V i, U ∈ 𝓝 x) : ∃ i, V i ⊆ U :=
  exists_subset_nhds_of_isCompact' hV hV_cpct (fun i => (hV_cpct i).isClosed) hU

Neighborhood Containment Property for Directed Families of Compact Sets in Hausdorff Spaces

Informal description

Let $X$ be a Hausdorff space and $\{V_i\}_{i \in \iota}$ be a nonempty directed family of compact subsets of $X$ with respect to reverse inclusion ($\supseteq$). If $U$ is a neighborhood of the intersection $\bigcap_{i \in \iota} V_i$ (i.e., for every $x \in \bigcap_{i \in \iota} V_i$, $U$ contains an open neighborhood of $x$), then there exists some index $i$ such that $V_i \subseteq U$.

CompactExhaustion.isClosed theorem

[T2Space X] (K : CompactExhaustion X) (n : ℕ) : IsClosed (K n)

Full source

theorem CompactExhaustion.isClosed [T2Space X] (K : CompactExhaustion X) (n : ℕ) : IsClosed (K n) :=
  (K.isCompact n).isClosed

Closedness of Compact Exhaustion Sets in Hausdorff Spaces

Informal description

Let $X$ be a Hausdorff space and let $(K_n)_{n \in \mathbb{N}}$ be a compact exhaustion of $X$. Then for every natural number $n$, the subset $K_n$ is closed in $X$.

IsCompact.inter theorem

[T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) : IsCompact (s ∩ t)

Full source

theorem IsCompact.inter [T2Space X] {s t : Set X} (hs : IsCompact s) (ht : IsCompact t) :
    IsCompact (s ∩ t) :=
  hs.inter_right <| ht.isClosed

Intersection of Compact Sets is Compact in Hausdorff Spaces

Informal description

In a Hausdorff space $X$, the intersection of any two compact subsets $s$ and $t$ is compact.

image_closure_of_isCompact theorem

 [T2Space Y] {s : Set X} (hs : IsCompact (closure s)) {f : X → Y} (hf : ContinuousOn f (closure s)) :
  f '' closure s = closure (f '' s)

Full source

theorem image_closure_of_isCompact [T2Space Y] {s : Set X} (hs : IsCompact (closure s)) {f : X → Y}
    (hf : ContinuousOn f (closure s)) : f '' closure s = closure (f '' s) :=
  Subset.antisymm hf.image_closure <|
    closure_minimal (image_subset f subset_closure) (hs.image_of_continuousOn hf).isClosed

Closure-Image Equality for Continuous Maps on Compact Closures in Hausdorff Spaces

Informal description

Let $X$ and $Y$ be topological spaces with $Y$ Hausdorff, and let $s \subseteq X$ be a subset whose closure is compact. If $f : X \to Y$ is continuous on the closure of $s$, then the image of the closure of $s$ under $f$ equals the closure of the image of $s$ under $f$, i.e., \[ f(\overline{s}) = \overline{f(s)}. \]

ContinuousAt.ne_iff_eventually_ne theorem

 [T2Space Y] {x : X} {f g : X → Y} (hf : ContinuousAt f x) (hg : ContinuousAt g x) : f x ≠ g x ↔ ∀ᶠ x in 𝓝 x, f x ≠ g x

Full source

/-- Two continuous maps into a Hausdorff space agree at a point iff they agree in a
neighborhood. -/
theorem ContinuousAt.ne_iff_eventually_ne [T2Space Y] {x : X} {f g : X → Y}
    (hf : ContinuousAt f x) (hg : ContinuousAt g x) :
    f x ≠ g xf x ≠ g x ↔ ∀ᶠ x in 𝓝 x, f x ≠ g x := by
  constructor <;> intro hfg
  · obtain ⟨Uf, Ug, h₁U, h₂U, h₃U, h₄U, h₅U⟩ := t2_separation hfg
    rw [Set.disjoint_iff_inter_eq_empty] at h₅U
    filter_upwards [inter_mem
      (hf.preimage_mem_nhds (IsOpen.mem_nhds h₁U h₃U))
      (hg.preimage_mem_nhds (IsOpen.mem_nhds h₂U h₄U))]
    intro x hx
    simp only [Set.mem_inter_iff, Set.mem_preimage] at hx
    by_contra H
    rw [H] at hx
    have : g x ∈ Uf ∩ Ug := hx
    simp [h₅U] at this
  · obtain ⟨t, h₁t, h₂t, h₃t⟩ := eventually_nhds_iff.1 hfg
    exact h₁t x h₃t

Neighborhood Characterization of Function Inequality at a Point in Hausdorff Spaces

Informal description

Let $Y$ be a Hausdorff space, $X$ a topological space, and $x \in X$. For any two continuous functions $f, g : X \to Y$ at $x$, we have $f(x) \neq g(x)$ if and only if $f$ and $g$ are not equal in some neighborhood of $x$. In other words, $f(x) \neq g(x) \iff \exists U \in \mathcal{N}(x), \forall y \in U, f(y) \neq g(y)$, where $\mathcal{N}(x)$ denotes the neighborhood filter at $x$.

ContinuousAt.eventuallyEq_nhd_iff_eventuallyEq_nhdNE theorem

 [T2Space Y] {x : X} {f g : X → Y} (hf : ContinuousAt f x) (hg : ContinuousAt g x) [(𝓝[≠] x).NeBot] :
  f =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g

Full source

/-- **Local identity principle** for continuous maps: Two continuous maps into a Hausdorff space
agree in a punctured neighborhood of a non-isolated point iff they agree in a neighborhood. -/
theorem ContinuousAt.eventuallyEq_nhd_iff_eventuallyEq_nhdNE [T2Space Y] {x : X} {f g : X → Y}
    (hf : ContinuousAt f x) (hg : ContinuousAt g x) [(𝓝[≠] x).NeBot] :
    f =ᶠ[𝓝[≠] x] gf =ᶠ[𝓝[≠] x] g ↔ f =ᶠ[𝓝 x] g := by
  constructor <;> intro hfg
  · apply eventuallyEq_nhds_of_eventuallyEq_nhdsNE hfg
    by_contra hCon
    obtain ⟨a, ha⟩ : {x | f x ≠ g x ∧ f x = g x}.Nonempty := by
      have h₁ := (eventually_nhdsWithin_of_eventually_nhds
        ((hf.ne_iff_eventually_ne hg).1 hCon)).and hfg
      have h₂ : ∅∅ ∉ 𝓝[≠] x := by exact empty_not_mem (𝓝[≠] x)
      simp_all
    simp at ha
  · exact hfg.filter_mono nhdsWithin_le_nhds

Local Identity Principle for Continuous Functions in Hausdorff Spaces

Informal description

Let $ Y $ be a Hausdorff space, $ X $ a topological space, and $ x \in X $ a non-isolated point (i.e., the punctured neighborhood filter $ \mathcal{N}_{≠}(x) $ is non-trivial). For any two functions $ f, g : X \to Y $ that are continuous at $ x $, the following are equivalent: 1. $ f $ and $ g $ agree on some punctured neighborhood of $ x $, i.e., $ f = g $ on $ \mathcal{N}_{≠}(x) $. 2. $ f $ and $ g $ agree on some full neighborhood of $ x $, i.e., $ f = g $ on $ \mathcal{N}(x) $.

Continuous.isClosedMap theorem

[CompactSpace X] [T2Space Y] {f : X → Y} (h : Continuous f) : IsClosedMap f

Full source

/-- A continuous map from a compact space to a Hausdorff space is a closed map. -/
protected theorem Continuous.isClosedMap [CompactSpace X] [T2Space Y] {f : X → Y}
    (h : Continuous f) : IsClosedMap f := fun _s hs => (hs.isCompact.image h).isClosed

Continuous Maps from Compact to Hausdorff Spaces are Closed

Informal description

Let $X$ be a compact topological space and $Y$ a Hausdorff space. If $f \colon X \to Y$ is a continuous map, then $f$ is a closed map, i.e., the image of any closed subset of $X$ under $f$ is closed in $Y$.

Continuous.isClosedEmbedding theorem

[CompactSpace X] [T2Space Y] {f : X → Y} (h : Continuous f) (hf : Function.Injective f) : IsClosedEmbedding f

Full source

/-- A continuous injective map from a compact space to a Hausdorff space is a closed embedding. -/
theorem Continuous.isClosedEmbedding [CompactSpace X] [T2Space Y] {f : X → Y} (h : Continuous f)
    (hf : Function.Injective f) : IsClosedEmbedding f :=
  .of_continuous_injective_isClosedMap h hf h.isClosedMap

Closed Embedding Theorem for Continuous Injective Maps from Compact to Hausdorff Spaces

Informal description

Let $X$ be a compact topological space and $Y$ a Hausdorff space. If $f \colon X \to Y$ is a continuous injective map, then $f$ is a closed embedding, meaning it is a homeomorphism onto its image and the image is closed in $Y$.

IsQuotientMap.of_surjective_continuous theorem

[CompactSpace X] [T2Space Y] {f : X → Y} (hsurj : Surjective f) (hcont : Continuous f) : IsQuotientMap f

Full source

/-- A continuous surjective map from a compact space to a Hausdorff space is a quotient map. -/
theorem IsQuotientMap.of_surjective_continuous [CompactSpace X] [T2Space Y] {f : X → Y}
    (hsurj : Surjective f) (hcont : Continuous f) : IsQuotientMap f :=
  hcont.isClosedMap.isQuotientMap hcont hsurj

Continuous Surjective Maps from Compact to Hausdorff Spaces are Quotient Maps

Informal description

Let $X$ be a compact topological space and $Y$ a Hausdorff space. If $f \colon X \to Y$ is a continuous surjective map, then $f$ is a quotient map, i.e., a subset $U \subseteq Y$ is open if and only if its preimage $f^{-1}(U)$ is open in $X$.

isPreirreducible_iff_subsingleton theorem

[T2Space X] {S : Set X} : IsPreirreducible S ↔ S.Subsingleton

Full source

theorem isPreirreducible_iff_subsingleton [T2Space X] {S : Set X} :
    IsPreirreducibleIsPreirreducible S ↔ S.Subsingleton := by
  refine ⟨fun h x hx y hy => ?_, Set.Subsingleton.isPreirreducible⟩
  by_contra e
  obtain ⟨U, V, hU, hV, hxU, hyV, h'⟩ := t2_separation e
  exact ((h U V hU hV ⟨x, hx, hxU⟩ ⟨y, hy, hyV⟩).mono inter_subset_right).not_disjoint h'

Preirreducible Sets in Hausdorff Spaces are Subsingletons

Informal description

Let $ X $ be a Hausdorff space and $ S $ a subset of $ X $. Then $ S $ is preirreducible (i.e., for any two nonempty open subsets $ U $ and $ V $ of $ S $, their intersection is nonempty) if and only if $ S $ is a subsingleton (i.e., contains at most one point).

IsPreirreducible.subsingleton theorem

[T2Space X] {S : Set X} (h : IsPreirreducible S) : S.Subsingleton

Full source

protected lemma IsPreirreducible.subsingleton [T2Space X] {S : Set X} (h : IsPreirreducible S) :
    S.Subsingleton :=
  isPreirreducible_iff_subsingleton.1 h

Preirreducible subsets in Hausdorff spaces are subsingletons

Informal description

Let $ X $ be a Hausdorff space and $ S $ a subset of $ X $. If $ S $ is preirreducible (i.e., any two nonempty open subsets of $ S $ have nonempty intersection), then $ S $ is a subsingleton (i.e., contains at most one point).

isIrreducible_iff_singleton theorem

[T2Space X] {S : Set X} : IsIrreducible S ↔ ∃ x, S = { x }

Full source

theorem isIrreducible_iff_singleton [T2Space X] {S : Set X} : IsIrreducibleIsIrreducible S ↔ ∃ x, S = {x} := by
  rw [IsIrreducible, isPreirreducible_iff_subsingleton,
    exists_eq_singleton_iff_nonempty_subsingleton]

Irreducible Sets in Hausdorff Spaces are Singletons

Informal description

Let $ X $ be a Hausdorff space and $ S $ a subset of $ X $. Then $ S $ is irreducible (i.e., nonempty and not the union of two proper closed subsets) if and only if $ S $ is a singleton set (i.e., there exists a point $ x \in X $ such that $ S = \{x\} $).

not_preirreducible_nontrivial_t2 theorem

(X) [TopologicalSpace X] [PreirreducibleSpace X] [Nontrivial X] [T2Space X] : False

Full source

/-- There does not exist a nontrivial preirreducible T₂ space. -/
theorem not_preirreducible_nontrivial_t2 (X) [TopologicalSpace X] [PreirreducibleSpace X]
    [Nontrivial X] [T2Space X] : False :=
  (PreirreducibleSpace.isPreirreducible_univ (X := X)).subsingleton.not_nontrivial nontrivial_univ

Nonexistence of Nontrivial Preirreducible Hausdorff Spaces

Informal description

There does not exist a nontrivial preirreducible Hausdorff space. In other words, if a topological space $ X $ is both preirreducible (any two nonempty open subsets intersect) and Hausdorff (T₂), then it must be trivial (i.e., contains at most one point).

t2Space_antitone theorem

{X : Type*} : Antitone (@T2Space X)

Full source

theorem t2Space_antitone {X : Type*} : Antitone (@T2Space X) :=
  fun inst₁ inst₂ h_top h_t2 ↦ @T2Space.of_injective_continuous _ _ inst₁ inst₂
    h_t2 _ Function.injective_id <| continuous_id_of_le h_top

Antitone Property of Hausdorff Spaces

Informal description

For any topological space $X$, the property of being a Hausdorff space is antitone with respect to the ordering of topologies on $X$. That is, if $\tau_1$ and $\tau_2$ are topologies on $X$ with $\tau_1 \subseteq \tau_2$, and $(X, \tau_2)$ is Hausdorff, then $(X, \tau_1)$ is also Hausdorff.

Mathlib.Topology.Separation.Hausdorff

Main definitions

Main results

T₂ spaces

References