doc-next-gen

Mathlib.Topology.Inseparable

Module docstring

{"# Inseparable points in a topological space

In this file we prove basic properties of the following notions defined elsewhere.

  • Specializes (notation: x ⤳ y) : a relation saying that 𝓝 x ≤ 𝓝 y;

  • Inseparable: a relation saying that two points in a topological space have the same neighbourhoods; equivalently, they can't be separated by an open set;

  • InseparableSetoid X: same relation, as a Setoid;

  • SeparationQuotient X: the quotient of X by its InseparableSetoid.

We also prove various basic properties of the relation Inseparable.

Notations

  • x ⤳ y: notation for Specializes x y;
  • x ~ᵢ y is used as a local notation for Inseparable x y;
  • 𝓝 x is the neighbourhoods filter nhds x of a point x, defined elsewhere.

Tags

topological space, separation setoid ","### Specializes relation ","### Inseparable relation ","### Separation quotient

In this section we define the quotient of a topological space by the Inseparable relation. "}

specializes_TFAE theorem
(x y : X) : TFAE [x ⤳ y, pure x ≤ 𝓝 y, ∀ s : Set X, IsOpen s → y ∈ s → x ∈ s, ∀ s : Set X, IsClosed s → x ∈ s → y ∈ s, y ∈ closure ({ x } : Set X), closure ({ y } : Set X) ⊆ closure { x }, ClusterPt y (pure x)]
Full source 
/-- A collection of equivalent definitions of `x ⤳ y`. The public API is given by `iff` lemmas
below. -/
theorem specializes_TFAE (x y : X) :
    TFAE [x ⤳ y,
      pure x ≤ 𝓝 y,
      ∀ s : Set X , IsOpen s → y ∈ s → x ∈ s,
      ∀ s : Set X , IsClosed s → x ∈ s → y ∈ s,
      y ∈ closure ({ x } : Set X),
      closure ({ y } : Set X) ⊆ closure { x },
      ClusterPt y (pure x)] := by
  tfae_have 1 → 2 := (pure_le_nhds _).trans
  tfae_have 2 → 3 := fun h s hso hy => h (hso.mem_nhds hy)
  tfae_have 3 → 4 := fun h s hsc hx => of_not_not fun hy => h sᶜ hsc.isOpen_compl hy hx
  tfae_have 4 → 5 := fun h => h _ isClosed_closure (subset_closure <| mem_singleton _)
  tfae_have 6 ↔ 5 := isClosed_closure.closure_subset_iff.trans singleton_subset_iff
  tfae_have 5 ↔ 7 := by
    rw [mem_closure_iff_clusterPt, principal_singleton]
  tfae_have 5 → 1 := by
    refine fun h => (nhds_basis_opens _).ge_iff.2 ?_
    rintro s ⟨hy, ho⟩
    rcases mem_closure_iff.1 h s ho hy with ⟨z, hxs, rfl : z = x⟩
    exact ho.mem_nhds hxs
  tfae_finish
Equivalent Characterizations of Specialization Relation $x \rightsquigarrow y$
Informal description
For any two points $x$ and $y$ in a topological space $X$, the following statements are equivalent: 1. $x$ specializes to $y$ (denoted $x \rightsquigarrow y$); 2. The principal ultrafilter at $x$ is contained in the neighborhood filter of $y$; 3. For every open set $s$ containing $y$, $x$ also belongs to $s$; 4. For every closed set $s$ containing $x$, $y$ also belongs to $s$; 5. $y$ belongs to the closure of the singleton set $\{x\}$; 6. The closure of $\{y\}$ is contained in the closure of $\{x\}$; 7. $y$ is a cluster point of the principal ultrafilter at $x$.
specializes_iff_nhds theorem
: x ⤳ y ↔ 𝓝 x ≤ 𝓝 y
Full source 
theorem specializes_iff_nhds : x ⤳ yx ⤳ y ↔ 𝓝 x ≤ 𝓝 y :=
  Iff.rfl
Specialization Relation Characterized by Neighborhood Filters
Informal description
For any two points $x$ and $y$ in a topological space $X$, the statement $x \rightsquigarrow y$ (read as "$x$ specializes to $y$") holds if and only if the neighborhood filter of $x$ is finer than the neighborhood filter of $y$, i.e., $\mathcal{N}_x \leq \mathcal{N}_y$.
Specializes.not_disjoint theorem
(h : x ⤳ y) : ¬Disjoint (𝓝 x) (𝓝 y)
Full source 
theorem Specializes.not_disjoint (h : x ⤳ y) : ¬Disjoint (𝓝 x) (𝓝 y) := fun hd ↦
  absurd (hd.mono_right h) <| by simp [NeBot.ne']
Non-disjoint Neighborhood Filters under Specialization
Informal description
If a point $x$ specializes to a point $y$ in a topological space (denoted $x \rightsquigarrow y$), then the neighborhood filters $\mathcal{N}(x)$ and $\mathcal{N}(y)$ are not disjoint.
specializes_iff_pure theorem
: x ⤳ y ↔ pure x ≤ 𝓝 y
Full source 
theorem specializes_iff_pure : x ⤳ yx ⤳ y ↔ pure x ≤ 𝓝 y :=
  (specializes_TFAE x y).out 0 1
Specialization Relation via Principal Ultrafilter and Neighborhood Filter
Informal description
For any two points $x$ and $y$ in a topological space $X$, the specialization relation $x \rightsquigarrow y$ holds if and only if the principal ultrafilter at $x$ is contained in the neighborhood filter of $y$, i.e., $\mathrm{pure}(x) \leq \mathcal{N}_y$.
ker_nhds_eq_specializes theorem
: (𝓝 x).ker = {y | y ⤳ x}
Full source 
theorem ker_nhds_eq_specializes : (𝓝 x).ker = {y | y ⤳ x} := by
  ext; simp [specializes_iff_pure, le_def]
Kernel of Neighborhood Filter Equals Specializing Points
Informal description
The kernel of the neighborhood filter $\mathcal{N}(x)$ at a point $x$ in a topological space is equal to the set of all points $y$ such that $y$ specializes to $x$ (denoted $y \rightsquigarrow x$), i.e., \[ \mathrm{ker}(\mathcal{N}(x)) = \{ y \mid y \rightsquigarrow x \}. \] Here, $\mathrm{ker}(\mathcal{N}(x))$ denotes the set of points whose neighborhood filter is finer than $\mathcal{N}(x)$, and $y \rightsquigarrow x$ means that every open neighborhood of $x$ is also a neighborhood of $y$.
Specializes.mem_open theorem
(h : x ⤳ y) (hs : IsOpen s) (hy : y ∈ s) : x ∈ s
Full source 
theorem Specializes.mem_open (h : x ⤳ y) (hs : IsOpen s) (hy : y ∈ s) : x ∈ s :=
  specializes_iff_forall_open.1 h s hs hy
Specialization Implies Membership in Open Sets
Informal description
For any two points $x$ and $y$ in a topological space $X$, if $x$ specializes to $y$ (denoted $x \rightsquigarrow y$) and $s$ is an open set containing $y$, then $x$ must also belong to $s$.
IsOpen.not_specializes theorem
(hs : IsOpen s) (hx : x ∉ s) (hy : y ∈ s) : ¬x ⤳ y
Full source 
theorem IsOpen.not_specializes (hs : IsOpen s) (hx : x ∉ s) (hy : y ∈ s) : ¬x ⤳ y := fun h =>
  hx <| h.mem_open hs hy
Open Set Separation Prevents Specialization
Informal description
For any open set $s$ in a topological space $X$, if $x \notin s$ and $y \in s$, then $x$ does not specialize to $y$ (i.e., $\neg(x \rightsquigarrow y)$).
specializes_iff_forall_closed theorem
: x ⤳ y ↔ ∀ s : Set X, IsClosed s → x ∈ s → y ∈ s
Full source 
theorem specializes_iff_forall_closed : x ⤳ yx ⤳ y ↔ ∀ s : Set X, IsClosed s → x ∈ s → y ∈ s :=
  (specializes_TFAE x y).out 0 3
Specialization Relation via Closed Sets
Informal description
For any two points $x$ and $y$ in a topological space $X$, the specialization relation $x \rightsquigarrow y$ holds if and only if for every closed set $s \subseteq X$, if $x \in s$ then $y \in s$.
Specializes.mem_closed theorem
(h : x ⤳ y) (hs : IsClosed s) (hx : x ∈ s) : y ∈ s
Full source 
theorem Specializes.mem_closed (h : x ⤳ y) (hs : IsClosed s) (hx : x ∈ s) : y ∈ s :=
  specializes_iff_forall_closed.1 h s hs hx
Specialization Implies Membership in Closed Sets
Informal description
Let $X$ be a topological space, and let $x, y \in X$ be points such that $x$ specializes to $y$ (denoted $x \rightsquigarrow y$). Then for any closed set $s \subseteq X$ containing $x$, we have $y \in s$.
IsClosed.not_specializes theorem
(hs : IsClosed s) (hx : x ∈ s) (hy : y ∉ s) : ¬x ⤳ y
Full source 
theorem IsClosed.not_specializes (hs : IsClosed s) (hx : x ∈ s) (hy : y ∉ s) : ¬x ⤳ y := fun h =>
  hy <| h.mem_closed hs hx
Closed Sets Prevent Specialization
Informal description
Let $X$ be a topological space, $s \subseteq X$ a closed set, and $x, y \in X$ points such that $x \in s$ and $y \notin s$. Then $x$ does not specialize to $y$ (i.e., $\neg (x \rightsquigarrow y)$).
specializes_iff_mem_closure theorem
: x ⤳ y ↔ y ∈ closure ({ x } : Set X)
Full source 
theorem specializes_iff_mem_closure : x ⤳ yx ⤳ y ↔ y ∈ closure ({x} : Set X) :=
  (specializes_TFAE x y).out 0 4
Specialization Relation Characterized by Closure Condition
Informal description
For any two points $x$ and $y$ in a topological space $X$, the specialization relation $x \rightsquigarrow y$ holds if and only if $y$ belongs to the closure of the singleton set $\{x\}$.
specializes_iff_closure_subset theorem
: x ⤳ y ↔ closure ({ y } : Set X) ⊆ closure { x }
Full source 
theorem specializes_iff_closure_subset : x ⤳ yx ⤳ y ↔ closure ({y} : Set X) ⊆ closure {x} :=
  (specializes_TFAE x y).out 0 5
Specialization Relation via Closure Containment
Informal description
For any two points $x$ and $y$ in a topological space $X$, the specialization relation $x \rightsquigarrow y$ holds if and only if the closure of the singleton set $\{y\}$ is contained in the closure of $\{x\}$.
specializes_iff_clusterPt theorem
: x ⤳ y ↔ ClusterPt y (pure x)
Full source 
theorem specializes_iff_clusterPt : x ⤳ yx ⤳ y ↔ ClusterPt y (pure x) :=
  (specializes_TFAE x y).out 0 6
Specialization Relation via Cluster Points of Principal Ultrafilter
Informal description
For any two points $x$ and $y$ in a topological space $X$, the specialization relation $x \rightsquigarrow y$ holds if and only if $y$ is a cluster point of the principal ultrafilter at $x$.
Filter.HasBasis.specializes_iff theorem
{ι} {p : ι → Prop} {s : ι → Set X} (h : (𝓝 y).HasBasis p s) : x ⤳ y ↔ ∀ i, p i → x ∈ s i
Full source 
theorem Filter.HasBasis.specializes_iff {ι} {p : ι → Prop} {s : ι → Set X}
    (h : (𝓝 y).HasBasis p s) : x ⤳ yx ⤳ y ↔ ∀ i, p i → x ∈ s i :=
  specializes_iff_pure.trans h.ge_iff
Specialization Relation via Neighborhood Basis
Informal description
Let $X$ be a topological space and let $\mathcal{N}_y$ be the neighborhood filter of a point $y \in X$. Suppose $\mathcal{N}_y$ has a basis $\{s_i\}_{i \in \iota}$ indexed by a type $\iota$ with a predicate $p : \iota \to \mathrm{Prop}$. Then for any $x \in X$, the specialization relation $x \rightsquigarrow y$ holds if and only if for every index $i$, if $p(i)$ is true, then $x$ belongs to the basis element $s_i$.
specializes_rfl theorem
: x ⤳ x
Full source 
theorem specializes_rfl : x ⤳ x := le_rfl
Reflexivity of the Specialization Relation
Informal description
For any point $x$ in a topological space, the specialization relation holds at $x$, i.e., $x \rightsquigarrow x$.
specializes_refl theorem
(x : X) : x ⤳ x
Full source 
@[refl]
theorem specializes_refl (x : X) : x ⤳ x :=
  specializes_rfl
Reflexivity of Specialization Relation
Informal description
For any point $x$ in a topological space $X$, the specialization relation holds at $x$, i.e., $x \rightsquigarrow x$.
Specializes.trans theorem
: x ⤳ y → y ⤳ z → x ⤳ z
Full source 
@[trans]
theorem Specializes.trans : x ⤳ y → y ⤳ z → x ⤳ z :=
  le_trans
Transitivity of Specialization Relation
Informal description
For any points $x$, $y$, and $z$ in a topological space, if $x$ specializes to $y$ and $y$ specializes to $z$, then $x$ specializes to $z$.
specializes_of_eq theorem
(e : x = y) : x ⤳ y
Full source 
theorem specializes_of_eq (e : x = y) : x ⤳ y :=
  e ▸ specializes_refl x
Specialization Relation Holds for Equal Points
Informal description
For any points $x$ and $y$ in a topological space, if $x = y$, then $x$ specializes to $y$ (i.e., $\mathfrak{N}(x) \leq \mathfrak{N}(y)$ where $\mathfrak{N}(x)$ denotes the neighborhood filter of $x$).
specializes_of_nhdsWithin theorem
(h₁ : 𝓝[s] x ≤ 𝓝[s] y) (h₂ : x ∈ s) : x ⤳ y
Full source 
theorem specializes_of_nhdsWithin (h₁ : 𝓝[s] x ≤ 𝓝[s] y) (h₂ : x ∈ s) : x ⤳ y :=
  specializes_iff_pure.2 <|
    calc
      pure x ≤ 𝓝[s] x := le_inf (pure_le_nhds _) (le_principal_iff.2 h₂)
      _ ≤ 𝓝[s] y := h₁
      _ ≤ 𝓝 y := inf_le_left
Specialization via Neighborhood Filters within a Subset
Informal description
For any subset $s$ of a topological space and points $x, y \in s$, if the neighborhood filter of $x$ within $s$ is less than or equal to the neighborhood filter of $y$ within $s$ (i.e., $\mathcal{N}_s(x) \leq \mathcal{N}_s(y)$), then $x$ specializes to $y$ (i.e., $x \rightsquigarrow y$).
Specializes.map_of_continuousAt theorem
(h : x ⤳ y) (hy : ContinuousAt f y) : f x ⤳ f y
Full source 
theorem Specializes.map_of_continuousAt (h : x ⤳ y) (hy : ContinuousAt f y) : f x ⤳ f y :=
  specializes_iff_pure.2 fun _s hs =>
    mem_pure.2 <| mem_preimage.1 <| mem_of_mem_nhds <| hy.mono_left h hs
Specialization is Preserved Under Continuous Functions at a Point
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, and $x, y \in X$. If $x$ specializes to $y$ (i.e., $\mathcal{N}_x \leq \mathcal{N}_y$) and $f$ is continuous at $y$, then $f(x)$ specializes to $f(y)$ in $Y$.
Specializes.map theorem
(h : x ⤳ y) (hf : Continuous f) : f x ⤳ f y
Full source 
theorem Specializes.map (h : x ⤳ y) (hf : Continuous f) : f x ⤳ f y :=
  h.map_of_continuousAt hf.continuousAt
Specialization is Preserved Under Continuous Functions
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a continuous function, and $x, y \in X$. If $x$ specializes to $y$ (i.e., $\mathcal{N}_x \leq \mathcal{N}_y$), then $f(x)$ specializes to $f(y)$ in $Y$.
Topology.IsInducing.specializes_iff theorem
(hf : IsInducing f) : f x ⤳ f y ↔ x ⤳ y
Full source 
theorem Topology.IsInducing.specializes_iff (hf : IsInducing f) : f x ⤳ f yf x ⤳ f y ↔ x ⤳ y := by
  simp only [specializes_iff_mem_closure, hf.closure_eq_preimage_closure_image, image_singleton,
    mem_preimage]
Specialization under Inducing Maps
Informal description
Let $f : X \to Y$ be an inducing map between topological spaces. For any points $x, y \in X$, the image $f(x)$ specializes to $f(y)$ in $Y$ if and only if $x$ specializes to $y$ in $X$.
subtype_specializes_iff theorem
{p : X → Prop} (x y : Subtype p) : x ⤳ y ↔ (x : X) ⤳ y
Full source 
theorem subtype_specializes_iff {p : X → Prop} (x y : Subtype p) : x ⤳ yx ⤳ y ↔ (x : X) ⤳ y :=
  IsInducing.subtypeVal.specializes_iff.symm
Specialization Relation in Subspace iff in Original Space
Informal description
For any subset $p$ of a topological space $X$ and any two points $x, y$ in the subspace topology on $p$, the specialization relation $x \rightsquigarrow y$ holds in the subspace if and only if it holds in the original space $X$.
specializes_prod theorem
{x₁ x₂ : X} {y₁ y₂ : Y} : (x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂
Full source 
@[simp]
theorem specializes_prod {x₁ x₂ : X} {y₁ y₂ : Y} : (x₁, y₁)(x₁, y₁) ⤳ (x₂, y₂)(x₁, y₁) ⤳ (x₂, y₂) ↔ x₁ ⤳ x₂ ∧ y₁ ⤳ y₂ := by
  simp only [Specializes, nhds_prod_eq, prod_le_prod]
Specialization in Product Space iff Component-wise Specialization
Informal description
For any points $x₁, x₂$ in a topological space $X$ and $y₁, y₂$ in a topological space $Y$, the pair $(x₁, y₁)$ specializes to $(x₂, y₂)$ in the product space $X × Y$ if and only if $x₁$ specializes to $x₂$ in $X$ and $y₁$ specializes to $y₂$ in $Y$. In other words, $(x₁, y₁) \rightsquigarrow (x₂, y₂) \leftrightarrow (x₁ \rightsquigarrow x₂) ∧ (y₁ \rightsquigarrow y₂)$.
Specializes.prod theorem
{x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ ⤳ x₂) (hy : y₁ ⤳ y₂) : (x₁, y₁) ⤳ (x₂, y₂)
Full source 
theorem Specializes.prod {x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ ⤳ x₂) (hy : y₁ ⤳ y₂) :
    (x₁, y₁)(x₁, y₁) ⤳ (x₂, y₂) :=
  specializes_prod.2 ⟨hx, hy⟩
Specialization in Product Space via Component-wise Specialization
Informal description
For any points $x₁, x₂$ in a topological space $X$ and $y₁, y₂$ in a topological space $Y$, if $x₁$ specializes to $x₂$ in $X$ and $y₁$ specializes to $y₂$ in $Y$, then the pair $(x₁, y₁)$ specializes to $(x₂, y₂)$ in the product space $X × Y$.
Specializes.fst theorem
{a b : X × Y} (h : a ⤳ b) : a.1 ⤳ b.1
Full source 
theorem Specializes.fst {a b : X × Y} (h : a ⤳ b) : a.1 ⤳ b.1 := (specializes_prod.1 h).1
Specialization Preserved Under First Projection
Informal description
For any points $a$ and $b$ in the product space $X \times Y$, if $a$ specializes to $b$ (i.e., $a \rightsquigarrow b$), then the first component of $a$ specializes to the first component of $b$ (i.e., $a.1 \rightsquigarrow b.1$).
Specializes.snd theorem
{a b : X × Y} (h : a ⤳ b) : a.2 ⤳ b.2
Full source 
theorem Specializes.snd {a b : X × Y} (h : a ⤳ b) : a.2 ⤳ b.2 := (specializes_prod.1 h).2
Specialization Preserved Under Second Projection in Product Space
Informal description
For any points $a$ and $b$ in the product space $X \times Y$, if $a$ specializes to $b$ (denoted $a \rightsquigarrow b$), then the second component of $a$ specializes to the second component of $b$ in $Y$, i.e., $a.2 \rightsquigarrow b.2$.
specializes_pi theorem
{f g : ∀ i, π i} : f ⤳ g ↔ ∀ i, f i ⤳ g i
Full source 
@[simp]
theorem specializes_pi {f g : ∀ i, π i} : f ⤳ gf ⤳ g ↔ ∀ i, f i ⤳ g i := by
  simp only [Specializes, nhds_pi, pi_le_pi]
Specialization in Product Space is Componentwise
Informal description
For any two functions $f, g$ in the product space $\prod_{i} \pi_i$, the relation $f \leadsto g$ (read as "$f$ specializes to $g$") holds if and only if for every index $i$, the component $f_i$ specializes to $g_i$ in the space $\pi_i$.
not_specializes_iff_exists_open theorem
: ¬x ⤳ y ↔ ∃ S : Set X, IsOpen S ∧ y ∈ S ∧ x ∉ S
Full source 
theorem not_specializes_iff_exists_open : ¬x ⤳ y¬x ⤳ y ↔ ∃ S : Set X, IsOpen S ∧ y ∈ S ∧ x ∉ S := by
  rw [specializes_iff_forall_open]
  push_neg
  rfl
Existence of Open Set Distinguishing Non-Specializing Points
Informal description
For any two points $x$ and $y$ in a topological space $X$, the negation of the specialization relation $x \rightsquigarrow y$ holds if and only if there exists an open set $S \subseteq X$ such that $y \in S$ and $x \notin S$.
not_specializes_iff_exists_closed theorem
: ¬x ⤳ y ↔ ∃ S : Set X, IsClosed S ∧ x ∈ S ∧ y ∉ S
Full source 
theorem not_specializes_iff_exists_closed : ¬x ⤳ y¬x ⤳ y ↔ ∃ S : Set X, IsClosed S ∧ x ∈ S ∧ y ∉ S := by
  rw [specializes_iff_forall_closed]
  push_neg
  rfl
Characterization of Non-Specialization via Closed Sets
Informal description
For any two points $x$ and $y$ in a topological space $X$, the negation of the specialization relation $x \rightsquigarrow y$ holds if and only if there exists a closed set $S \subseteq X$ such that $x \in S$ and $y \notin S$.
IsOpen.continuous_piecewise_of_specializes theorem
[DecidablePred (· ∈ s)] (hs : IsOpen s) (hf : Continuous f) (hg : Continuous g) (hspec : ∀ x, f x ⤳ g x) : Continuous (s.piecewise f g)
Full source 
theorem IsOpen.continuous_piecewise_of_specializes [DecidablePred (· ∈ s)] (hs : IsOpen s)
    (hf : Continuous f) (hg : Continuous g) (hspec : ∀ x, f x ⤳ g x) :
    Continuous (s.piecewise f g) := by
  have : ∀ U, IsOpen U → g ⁻¹' Ug ⁻¹' U ⊆ f ⁻¹' U := fun U hU x hx ↦ (hspec x).mem_open hU hx
  rw [continuous_def]
  intro U hU
  rw [piecewise_preimage, ite_eq_of_subset_right _ (this U hU)]
  exact hU.preimage hf |>.inter hs |>.union (hU.preimage hg)
Continuity of Piecewise Function with Specialization Condition on Open Set
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ be an open set, and $f, g : X \to Y$ be continuous functions. Suppose that for every $x \in X$, $f(x)$ specializes to $g(x)$. Then the piecewise function defined by \[ h(x) = \begin{cases} f(x) & \text{if } x \in s, \\ g(x) & \text{otherwise}, \end{cases} \] is continuous.
IsClosed.continuous_piecewise_of_specializes theorem
[DecidablePred (· ∈ s)] (hs : IsClosed s) (hf : Continuous f) (hg : Continuous g) (hspec : ∀ x, g x ⤳ f x) : Continuous (s.piecewise f g)
Full source 
theorem IsClosed.continuous_piecewise_of_specializes [DecidablePred (· ∈ s)] (hs : IsClosed s)
    (hf : Continuous f) (hg : Continuous g) (hspec : ∀ x, g x ⤳ f x) :
    Continuous (s.piecewise f g) := by
  simpa only [piecewise_compl] using hs.isOpen_compl.continuous_piecewise_of_specializes hg hf hspec
Continuity of Piecewise Function with Specialization Condition on Closed Set
Informal description
Let $X$ and $Y$ be topological spaces, $s \subseteq X$ be a closed set, and $f, g : X \to Y$ be continuous functions. Suppose that for every $x \in X$, $g(x)$ specializes to $f(x)$. Then the piecewise function defined by \[ h(x) = \begin{cases} f(x) & \text{if } x \in s, \\ g(x) & \text{otherwise}, \end{cases} \] is continuous.
Continuous.specialization_monotone theorem
(hf : Continuous f) : Monotone f
Full source 
/-- A continuous function is monotone with respect to the specialization preorders on the domain and
the codomain. -/
theorem Continuous.specialization_monotone (hf : Continuous f) : Monotone f :=
  fun _ _ h => h.map hf
Continuous Functions are Monotone with Respect to Specialization Preorders
Informal description
Let $X$ and $Y$ be topological spaces and $f : X \to Y$ a continuous function. Then $f$ is monotone with respect to the specialization preorders on $X$ and $Y$, i.e., for any $x, y \in X$, if $x$ specializes to $y$ (denoted $x \rightsquigarrow y$), then $f(x)$ specializes to $f(y)$ (denoted $f(x) \rightsquigarrow f(y)$).
closure_singleton_eq_Iic theorem
(x : X) : closure { x } = Iic x
Full source 
lemma closure_singleton_eq_Iic (x : X) : closure {x} = Iic x :=
  Set.ext fun _ ↦ specializes_iff_mem_closure.symm
Closure of Singleton Equals Specialization Order Interval
Informal description
For any point $x$ in a topological space $X$, the closure of the singleton set $\{x\}$ is equal to the left-infinite right-closed interval $(-\infty, x]$, where the interval is defined with respect to the specialization order on $X$.
StableUnderSpecialization definition
(s : Set X) : Prop
Full source 
/-- A subset `S` of a topological space is stable under specialization
if `x ∈ S → y ∈ S` for all `x ⤳ y`. -/
def StableUnderSpecialization (s : Set X) : Prop :=
  ∀ ⦃x y⦄, x ⤳ y → x ∈ s → y ∈ s
Stable under specialization
Informal description
A subset $S$ of a topological space $X$ is called *stable under specialization* if for any points $x, y \in X$ such that $x$ specializes to $y$ (denoted $x \rightsquigarrow y$, meaning every neighborhood of $y$ is a neighborhood of $x$), whenever $x \in S$, then $y \in S$ as well.
StableUnderGeneralization definition
(s : Set X) : Prop
Full source 
/-- A subset `S` of a topological space is stable under specialization
if `x ∈ S → y ∈ S` for all `y ⤳ x`. -/
def StableUnderGeneralization (s : Set X) : Prop :=
  ∀ ⦃x y⦄, y ⤳ x → x ∈ s → y ∈ s
Stable under generalization
Informal description
A subset $S$ of a topological space is stable under generalization if for any points $x$ and $y$ such that $y$ specializes to $x$ (i.e., the neighborhood filter of $y$ is contained in that of $x$), whenever $x$ belongs to $S$, then $y$ also belongs to $S$.
IsClosed.stableUnderSpecialization theorem
{s : Set X} (hs : IsClosed s) : StableUnderSpecialization s
Full source 
lemma IsClosed.stableUnderSpecialization {s : Set X} (hs : IsClosed s) :
    StableUnderSpecialization s :=
  fun _ _ e ↦ e.mem_closed hs
Closed Sets are Stable Under Specialization
Informal description
For any closed subset $s$ of a topological space $X$, the set $s$ is stable under specialization. That is, for any points $x, y \in X$ such that $x$ specializes to $y$ (denoted $x \rightsquigarrow y$), if $x \in s$, then $y \in s$.
IsOpen.stableUnderGeneralization theorem
{s : Set X} (hs : IsOpen s) : StableUnderGeneralization s
Full source 
lemma IsOpen.stableUnderGeneralization {s : Set X} (hs : IsOpen s) :
    StableUnderGeneralization s :=
  fun _ _ e ↦ e.mem_open hs
Open Sets are Stable Under Generalization
Informal description
For any open subset $s$ of a topological space $X$, the set $s$ is stable under generalization, meaning that if $x \rightsquigarrow y$ (i.e., $x$ specializes to $y$) and $y \in s$, then $x \in s$.
stableUnderSpecialization_compl_iff theorem
{s : Set X} : StableUnderSpecialization sᶜ ↔ StableUnderGeneralization s
Full source 
@[simp]
lemma stableUnderSpecialization_compl_iff {s : Set X} :
    StableUnderSpecializationStableUnderSpecialization sᶜ ↔ StableUnderGeneralization s :=
  isLowerSet_compl
Complement Stability Under Specialization ↔ Generalization Stability
Informal description
For any subset $s$ of a topological space $X$, the complement $s^c$ is stable under specialization if and only if $s$ is stable under generalization. Here, a set is *stable under specialization* if for any points $x \rightsquigarrow y$ (i.e., $x$ specializes to $y$), $x \in s^c$ implies $y \in s^c$, and a set is *stable under generalization* if for any $x \rightsquigarrow y$, $y \in s$ implies $x \in s$.
stableUnderGeneralization_compl_iff theorem
{s : Set X} : StableUnderGeneralization sᶜ ↔ StableUnderSpecialization s
Full source 
@[simp]
lemma stableUnderGeneralization_compl_iff {s : Set X} :
    StableUnderGeneralizationStableUnderGeneralization sᶜ ↔ StableUnderSpecialization s :=
  isUpperSet_compl
Complement Stability Under Generalization ↔ Specialization Stability
Informal description
For any subset $s$ of a topological space $X$, the complement $s^c$ is stable under generalization if and only if $s$ is stable under specialization. Here, a set is *stable under generalization* if for any points $x \rightsquigarrow y$ (i.e., $x$ specializes to $y$), $y \in s^c$ implies $x \in s^c$, and a set is *stable under specialization* if for any $x \rightsquigarrow y$, $x \in s$ implies $y \in s$.
stableUnderSpecialization_univ theorem
: StableUnderSpecialization (univ : Set X)
Full source 
lemma stableUnderSpecialization_univ : StableUnderSpecialization (univ : Set X) := isLowerSet_univ
Universal Set is Stable Under Specialization
Informal description
The universal set $\text{univ}$ in a topological space $X$ is stable under specialization. That is, for any points $x, y \in X$ such that $x$ specializes to $y$ (denoted $x \rightsquigarrow y$, meaning every neighborhood of $y$ is a neighborhood of $x$), if $x \in \text{univ}$, then $y \in \text{univ}$.
stableUnderSpecialization_empty theorem
: StableUnderSpecialization (∅ : Set X)
Full source 
lemma stableUnderSpecialization_empty : StableUnderSpecialization (∅ : Set X) := isLowerSet_empty
Empty Set is Stable Under Specialization
Informal description
The empty set $\emptyset$ in a topological space $X$ is stable under specialization. That is, for any points $x, y \in X$ such that $x$ specializes to $y$ (denoted $x \rightsquigarrow y$, meaning every neighborhood of $y$ is a neighborhood of $x$), if $x \in \emptyset$, then $y \in \emptyset$.
stableUnderGeneralization_univ theorem
: StableUnderGeneralization (univ : Set X)
Full source 
lemma stableUnderGeneralization_univ : StableUnderGeneralization (univ : Set X) := isUpperSet_univ
Universal Set is Stable Under Generalization
Informal description
The universal set $\text{univ}$ in a topological space $X$ is stable under generalization. That is, for any points $x, y \in X$ such that $x$ specializes to $y$ (i.e., the neighborhood filter of $x$ is contained in that of $y$), if $y \in \text{univ}$, then $x \in \text{univ}$.
stableUnderGeneralization_empty theorem
: StableUnderGeneralization (∅ : Set X)
Full source 
lemma stableUnderGeneralization_empty : StableUnderGeneralization (∅ : Set X) := isUpperSet_empty
Empty Set is Stable Under Generalization
Informal description
The empty set $\emptyset$ in a topological space $X$ is stable under generalization, meaning that for any points $x, y \in X$ such that $x$ specializes to $y$ (i.e., the neighborhood filter of $x$ is contained in that of $y$), if $y \in \emptyset$, then $x \in \emptyset$.
stableUnderSpecialization_sUnion theorem
(S : Set (Set X)) (H : ∀ s ∈ S, StableUnderSpecialization s) : StableUnderSpecialization (⋃₀ S)
Full source 
lemma stableUnderSpecialization_sUnion (S : Set (Set X))
    (H : ∀ s ∈ S, StableUnderSpecialization s) : StableUnderSpecialization (⋃₀ S) :=
  isLowerSet_sUnion H
Union of Specialization-Stable Sets is Specialization-Stable
Informal description
Let $X$ be a topological space and $S$ be a collection of subsets of $X$. If every subset in $S$ is stable under specialization (i.e., for any $x, y \in X$ with $x \rightsquigarrow y$, if $x \in s$ then $y \in s$ for each $s \in S$), then the union $\bigcup_{s \in S} s$ is also stable under specialization.
stableUnderSpecialization_sInter theorem
(S : Set (Set X)) (H : ∀ s ∈ S, StableUnderSpecialization s) : StableUnderSpecialization (⋂₀ S)
Full source 
lemma stableUnderSpecialization_sInter (S : Set (Set X))
    (H : ∀ s ∈ S, StableUnderSpecialization s) : StableUnderSpecialization (⋂₀ S) :=
  isLowerSet_sInter H
Intersection of Specialization-Stable Sets is Specialization-Stable
Informal description
Let $X$ be a topological space and $S$ be a collection of subsets of $X$. If every subset $s \in S$ is stable under specialization (i.e., for any $x, y \in X$ with $x \rightsquigarrow y$, if $x \in s$ then $y \in s$), then the intersection $\bigcap_{s \in S} s$ is also stable under specialization.
stableUnderGeneralization_sUnion theorem
(S : Set (Set X)) (H : ∀ s ∈ S, StableUnderGeneralization s) : StableUnderGeneralization (⋃₀ S)
Full source 
lemma stableUnderGeneralization_sUnion (S : Set (Set X))
    (H : ∀ s ∈ S, StableUnderGeneralization s) : StableUnderGeneralization (⋃₀ S) :=
  isUpperSet_sUnion H
Union of Generalization-Stable Sets is Generalization-Stable
Informal description
Let $X$ be a topological space and $S$ be a collection of subsets of $X$. If every subset $s \in S$ is stable under generalization (i.e., for any $x, y \in X$ with $y \rightsquigarrow x$, if $x \in s$ then $y \in s$ for each $s \in S$), then the union $\bigcup_{s \in S} s$ is also stable under generalization.
stableUnderGeneralization_sInter theorem
(S : Set (Set X)) (H : ∀ s ∈ S, StableUnderGeneralization s) : StableUnderGeneralization (⋂₀ S)
Full source 
lemma stableUnderGeneralization_sInter (S : Set (Set X))
    (H : ∀ s ∈ S, StableUnderGeneralization s) : StableUnderGeneralization (⋂₀ S) :=
  isUpperSet_sInter H
Intersection of Generalization-Stable Sets is Generalization-Stable
Informal description
Let $X$ be a topological space and $S$ be a collection of subsets of $X$. If every subset $s \in S$ is stable under generalization (i.e., for any $x, y \in X$ with $y \rightsquigarrow x$, if $x \in s$ then $y \in s$), then the intersection $\bigcap_{s \in S} s$ is also stable under generalization.
stableUnderSpecialization_iUnion theorem
{ι : Sort*} (S : ι → Set X) (H : ∀ i, StableUnderSpecialization (S i)) : StableUnderSpecialization (⋃ i, S i)
Full source 
lemma stableUnderSpecialization_iUnion {ι : Sort*} (S : ι → Set X)
    (H : ∀ i, StableUnderSpecialization (S i)) : StableUnderSpecialization (⋃ i, S i) :=
  isLowerSet_iUnion H
Union of Specialization-Stable Sets is Specialization-Stable
Informal description
Let $X$ be a topological space and $\{S_i\}_{i \in \iota}$ be a family of subsets of $X$ such that each $S_i$ is stable under specialization. Then the union $\bigcup_{i \in \iota} S_i$ is also stable under specialization.
stableUnderSpecialization_iInter theorem
{ι : Sort*} (S : ι → Set X) (H : ∀ i, StableUnderSpecialization (S i)) : StableUnderSpecialization (⋂ i, S i)
Full source 
lemma stableUnderSpecialization_iInter {ι : Sort*} (S : ι → Set X)
    (H : ∀ i, StableUnderSpecialization (S i)) : StableUnderSpecialization (⋂ i, S i) :=
  isLowerSet_iInter H
Intersection of Specialization-Stable Sets is Specialization-Stable
Informal description
Let $X$ be a topological space and $\{S_i\}_{i \in \iota}$ be a family of subsets of $X$ such that each $S_i$ is stable under specialization (i.e., for any $x, y \in X$ with $x \rightsquigarrow y$, if $x \in S_i$ then $y \in S_i$). Then the intersection $\bigcap_{i \in \iota} S_i$ is also stable under specialization.
stableUnderGeneralization_iUnion theorem
{ι : Sort*} (S : ι → Set X) (H : ∀ i, StableUnderGeneralization (S i)) : StableUnderGeneralization (⋃ i, S i)
Full source 
lemma stableUnderGeneralization_iUnion {ι : Sort*} (S : ι → Set X)
    (H : ∀ i, StableUnderGeneralization (S i)) : StableUnderGeneralization (⋃ i, S i) :=
  isUpperSet_iUnion H
Union of Generalization-Stable Sets is Generalization-Stable
Informal description
Let $X$ be a topological space and $\{S_i\}_{i \in \iota}$ be a family of subsets of $X$ such that each $S_i$ is stable under generalization (i.e., for any $x, y \in X$ with $y \rightsquigarrow x$, if $x \in S_i$ then $y \in S_i$). Then the union $\bigcup_{i \in \iota} S_i$ is also stable under generalization.
stableUnderGeneralization_iInter theorem
{ι : Sort*} (S : ι → Set X) (H : ∀ i, StableUnderGeneralization (S i)) : StableUnderGeneralization (⋂ i, S i)
Full source 
lemma stableUnderGeneralization_iInter {ι : Sort*} (S : ι → Set X)
    (H : ∀ i, StableUnderGeneralization (S i)) : StableUnderGeneralization (⋂ i, S i) :=
  isUpperSet_iInter H
Intersection of Generalization-Stable Sets is Generalization-Stable
Informal description
Let $X$ be a topological space and $\{S_i\}_{i \in \iota}$ be a family of subsets of $X$ such that each $S_i$ is stable under generalization (i.e., for any $x, y \in X$ with $y \rightsquigarrow x$, if $x \in S_i$ then $y \in S_i$). Then the intersection $\bigcap_{i \in \iota} S_i$ is also stable under generalization.
Union_closure_singleton_eq_iff theorem
{s : Set X} : (⋃ x ∈ s, closure { x }) = s ↔ StableUnderSpecialization s
Full source 
lemma Union_closure_singleton_eq_iff {s : Set X} :
    (⋃ x ∈ s, closure {x}) = s ↔ StableUnderSpecialization s :=
  show _ ↔ IsLowerSet s by simp only [closure_singleton_eq_Iic, ← lowerClosure_eq, coe_lowerClosure]
Characterization of Specialization-Stable Sets via Union of Singleton Closures
Informal description
For any subset $s$ of a topological space $X$, the union of the closures of all singleton sets $\{x\}$ for $x \in s$ equals $s$ if and only if $s$ is stable under specialization. That is, \[ \bigcup_{x \in s} \overline{\{x\}} = s \leftrightarrow \text{StableUnderSpecialization}(s). \]
stableUnderSpecialization_iff_Union_eq theorem
{s : Set X} : StableUnderSpecialization s ↔ (⋃ x ∈ s, closure { x }) = s
Full source 
lemma stableUnderSpecialization_iff_Union_eq {s : Set X} :
    StableUnderSpecializationStableUnderSpecialization s ↔ (⋃ x ∈ s, closure {x}) = s :=
  Union_closure_singleton_eq_iff.symm
Characterization of Specialization-Stable Sets via Union of Singleton Closures
Informal description
A subset $s$ of a topological space $X$ is stable under specialization if and only if it equals the union of the closures of all its singleton subsets. That is, \[ \text{StableUnderSpecialization}(s) \leftrightarrow \bigcup_{x \in s} \overline{\{x\}} = s. \]
stableUnderSpecialization_iff_exists_sUnion_eq theorem
{s : Set X} : StableUnderSpecialization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed s) ∧ ⋃₀ S = s
Full source 
/-- A set is stable under specialization iff it is a union of closed sets. -/
lemma stableUnderSpecialization_iff_exists_sUnion_eq {s : Set X} :
    StableUnderSpecializationStableUnderSpecialization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsClosed s) ∧ ⋃₀ S = s := by
  refine ⟨fun H ↦ ⟨(fun x : X ↦ closure {x}) '' s, ?_, ?_⟩, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderSpecialization_sUnion S (fun x hx ↦ (hS x hx).stableUnderSpecialization)⟩
  · rintro _ ⟨_, _, rfl⟩; exact isClosed_closure
  · conv_rhs => rw [← H.Union_eq]
    simp
Characterization of Specialization-Stable Sets as Union of Closed Sets
Informal description
A subset $s$ of a topological space $X$ is stable under specialization if and only if there exists a collection $S$ of closed subsets of $X$ such that $s$ is equal to the union of all sets in $S$. In other words, \[ \text{StableUnderSpecialization}(s) \leftrightarrow \exists S \subseteq \mathcal{P}(X), (\forall t \in S, \text{IsClosed}(t)) \land \bigcup S = s. \]
stableUnderGeneralization_iff_exists_sInter_eq theorem
{s : Set X} : StableUnderGeneralization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s
Full source 
/-- A set is stable under generalization iff it is an intersection of open sets. -/
lemma stableUnderGeneralization_iff_exists_sInter_eq {s : Set X} :
    StableUnderGeneralizationStableUnderGeneralization s ↔ ∃ (S : Set (Set X)), (∀ s ∈ S, IsOpen s) ∧ ⋂₀ S = s := by
  refine ⟨?_, fun ⟨S, hS, e⟩ ↦ e ▸
    stableUnderGeneralization_sInter S (fun x hx ↦ (hS x hx).stableUnderGeneralization)⟩
  rw [← stableUnderSpecialization_compl_iff, stableUnderSpecialization_iff_exists_sUnion_eq]
  exact fun ⟨S, h₁, h₂⟩ ↦ ⟨(·ᶜ) '' S, fun s ⟨t, ht, e⟩ ↦ e ▸ (h₁ t ht).isOpen_compl,
    compl_injective ((sUnion_eq_compl_sInter_compl S).symm.trans h₂)⟩
Characterization of Generalization-Stable Sets as Intersection of Open Sets
Informal description
A subset $s$ of a topological space $X$ is stable under generalization if and only if there exists a collection $S$ of open subsets of $X$ such that $s$ is equal to the intersection of all sets in $S$. In other words, \[ \text{StableUnderGeneralization}(s) \leftrightarrow \exists S \subseteq \mathcal{P}(X), (\forall t \in S, \text{IsOpen}(t)) \land \bigcap S = s. \]
StableUnderSpecialization.preimage theorem
{s : Set Y} (hs : StableUnderSpecialization s) (hf : Continuous f) : StableUnderSpecialization (f ⁻¹' s)
Full source 
lemma StableUnderSpecialization.preimage {s : Set Y}
    (hs : StableUnderSpecialization s) (hf : Continuous f) :
    StableUnderSpecialization (f ⁻¹' s) :=
  IsLowerSet.preimage hs hf.specialization_monotone
Preimage of a Specialization-Stable Set under Continuous Map is Specialization-Stable
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a continuous function, and $s \subseteq Y$ a subset that is stable under specialization. Then the preimage $f^{-1}(s) \subseteq X$ is also stable under specialization.
StableUnderGeneralization.preimage theorem
{s : Set Y} (hs : StableUnderGeneralization s) (hf : Continuous f) : StableUnderGeneralization (f ⁻¹' s)
Full source 
lemma StableUnderGeneralization.preimage {s : Set Y}
    (hs : StableUnderGeneralization s) (hf : Continuous f) :
    StableUnderGeneralization (f ⁻¹' s) :=
  IsUpperSet.preimage hs hf.specialization_monotone
Preimage of a generalization-stable set under a continuous map is generalization-stable
Informal description
Let $X$ and $Y$ be topological spaces, $f \colon X \to Y$ a continuous function, and $s \subseteq Y$ a subset that is stable under generalization. Then the preimage $f^{-1}(s) \subseteq X$ is also stable under generalization.
SpecializingMap definition
(f : X → Y) : Prop
Full source 
/-- A map `f` between topological spaces is specializing if specializations lifts along `f`,
i.e. for each `f x' ⤳ y` there is some `x` with `x' ⤳ x` whose image is `y`. -/
def SpecializingMap (f : X → Y) : Prop :=
  Relation.Fibration (flip (· ⤳ ·)) (flip (· ⤳ ·)) f
Specializing map
Informal description
A continuous map $f \colon X \to Y$ between topological spaces is called *specializing* if for every point $x' \in X$ and every point $y \in Y$ such that $y$ specializes to $f(x')$ (i.e., $y$ is in the closure of $\{f(x')\}$), there exists a point $x \in X$ such that $x'$ specializes to $x$ (i.e., $x$ is in the closure of $\{x'\}$) and $f(x) = y$. Equivalently, $f$ is specializing if for every $x \in X$, the image of the closure of $\{x\}$ under $f$ contains the closure of $\{f(x)\}$.
GeneralizingMap definition
(f : X → Y) : Prop
Full source 
/-- A map `f` between topological spaces is generalizing if generalizations lifts along `f`,
i.e. for each `y ⤳ f x'` there is some `x ⤳ x'` whose image is `y`. -/
def GeneralizingMap (f : X → Y) : Prop :=
  Relation.Fibration (· ⤳ ·) (· ⤳ ·) f
Generalizing map between topological spaces
Informal description
A function $f \colon X \to Y$ between topological spaces is called *generalizing* if for every point $x' \in X$ and every point $y \in Y$ such that $y$ specializes to $f(x')$ (i.e., the neighborhood filter of $y$ is contained in that of $f(x')$), there exists a point $x \in X$ specializing to $x'$ such that $f(x) = y$. In other words, specializations lift along $f$.
specializingMap_iff_closure_singleton_subset theorem
: SpecializingMap f ↔ ∀ x, closure {f x} ⊆ f '' closure { x }
Full source 
lemma specializingMap_iff_closure_singleton_subset :
    SpecializingMapSpecializingMap f ↔ ∀ x, closure {f x} ⊆ f '' closure {x} := by
  simp only [SpecializingMap, Relation.Fibration, flip, specializes_iff_mem_closure]; rfl
Specializing Map Characterization via Closure of Singletons
Informal description
A continuous map $f \colon X \to Y$ between topological spaces is specializing if and only if for every point $x \in X$, the closure of the singleton $\{f(x)\}$ is contained in the image under $f$ of the closure of $\{x\}$.
SpecializingMap.stableUnderSpecialization_image theorem
(hf : SpecializingMap f) {s : Set X} (hs : StableUnderSpecialization s) : StableUnderSpecialization (f '' s)
Full source 
lemma SpecializingMap.stableUnderSpecialization_image (hf : SpecializingMap f)
    {s : Set X} (hs : StableUnderSpecialization s) : StableUnderSpecialization (f '' s) :=
  IsLowerSet.image_fibration hf hs
Image of Specialization-Stable Set under Specializing Map is Specialization-Stable
Informal description
Let $f \colon X \to Y$ be a specializing map between topological spaces, and let $s \subseteq X$ be a subset that is stable under specialization. Then the image $f(s) \subseteq Y$ is also stable under specialization.
specializingMap_iff_stableUnderSpecialization_image_singleton theorem
: SpecializingMap f ↔ ∀ x, StableUnderSpecialization (f '' closure { x })
Full source 
lemma specializingMap_iff_stableUnderSpecialization_image_singleton :
    SpecializingMapSpecializingMap f ↔ ∀ x, StableUnderSpecialization (f '' closure {x}) := by
  simpa only [closure_singleton_eq_Iic] using Relation.fibration_iff_isLowerSet_image_Iic
Specializing Map Characterization via Specialization-Stability of Point Closures' Images
Informal description
A continuous map $f \colon X \to Y$ between topological spaces is specializing if and only if for every point $x \in X$, the image of the closure of $\{x\}$ under $f$ is stable under specialization in $Y$. Here, a set is stable under specialization if whenever it contains a point $y$, it also contains all points that specialize to $y$.
specializingMap_iff_stableUnderSpecialization_image theorem
: SpecializingMap f ↔ ∀ s, StableUnderSpecialization s → StableUnderSpecialization (f '' s)
Full source 
lemma specializingMap_iff_stableUnderSpecialization_image :
    SpecializingMapSpecializingMap f ↔ ∀ s, StableUnderSpecialization s → StableUnderSpecialization (f '' s) :=
  Relation.fibration_iff_isLowerSet_image
Characterization of Specializing Maps via Stability Under Specialization of Images
Informal description
A continuous map $f \colon X \to Y$ between topological spaces is a specializing map if and only if for every subset $s \subseteq X$ that is stable under specialization (i.e., if $x \in s$ and $x \rightsquigarrow y$, then $y \in s$), the image $f(s)$ is also stable under specialization in $Y$.
specializingMap_iff_closure_singleton theorem
(hf : Continuous f) : SpecializingMap f ↔ ∀ x, f '' closure { x } = closure {f x}
Full source 
lemma specializingMap_iff_closure_singleton (hf : Continuous f) :
    SpecializingMapSpecializingMap f ↔ ∀ x, f '' closure {x} = closure {f x} := by
  simpa only [closure_singleton_eq_Iic] using
    Relation.fibration_iff_image_Iic hf.specialization_monotone
Characterization of Specializing Maps via Closure of Singletons
Informal description
Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ a continuous function. Then $f$ is a specializing map if and only if for every point $x \in X$, the image under $f$ of the closure of $\{x\}$ equals the closure of $\{f(x)\}$ in $Y$.
specializingMap_iff_isClosed_image_closure_singleton theorem
(hf : Continuous f) : SpecializingMap f ↔ ∀ x, IsClosed (f '' closure { x })
Full source 
lemma specializingMap_iff_isClosed_image_closure_singleton (hf : Continuous f) :
    SpecializingMapSpecializingMap f ↔ ∀ x, IsClosed (f '' closure {x}) := by
  refine ⟨fun h x ↦ ?_, fun h ↦ specializingMap_iff_stableUnderSpecialization_image_singleton.mpr
    (fun x ↦ (h x).stableUnderSpecialization)⟩
  rw [(specializingMap_iff_closure_singleton hf).mp h x]
  exact isClosed_closure
Characterization of Specializing Maps via Closedness of Point Closure Images
Informal description
Let $X$ and $Y$ be topological spaces and $f \colon X \to Y$ a continuous function. Then $f$ is a specializing map if and only if for every point $x \in X$, the image under $f$ of the closure of $\{x\}$ is closed in $Y$.
SpecializingMap.comp theorem
{f : X → Y} {g : Y → Z} (hf : SpecializingMap f) (hg : SpecializingMap g) : SpecializingMap (g ∘ f)
Full source 
lemma SpecializingMap.comp {f : X → Y} {g : Y → Z}
    (hf : SpecializingMap f) (hg : SpecializingMap g) :
    SpecializingMap (g ∘ f) := by
  simp only [specializingMap_iff_stableUnderSpecialization_image, Set.image_comp] at *
  exact fun s h ↦ hg _ (hf  _ h)
Composition of Specializing Maps is Specializing
Informal description
Let $f \colon X \to Y$ and $g \colon Y \to Z$ be specializing maps between topological spaces. Then the composition $g \circ f \colon X \to Z$ is also a specializing map.
IsClosedMap.specializingMap theorem
(hf : IsClosedMap f) : SpecializingMap f
Full source 
lemma IsClosedMap.specializingMap (hf : IsClosedMap f) : SpecializingMap f :=
  specializingMap_iff_stableUnderSpecialization_image_singleton.mpr <|
    fun _ ↦ (hf _ isClosed_closure).stableUnderSpecialization
Closed Maps are Specializing
Informal description
If $f \colon X \to Y$ is a closed map between topological spaces, then $f$ is a specializing map. That is, for every point $x' \in X$ and every point $y \in Y$ such that $y$ specializes to $f(x')$, there exists a point $x \in X$ such that $x'$ specializes to $x$ and $f(x) = y$.
Topology.IsInducing.specializingMap theorem
(hf : IsInducing f) (h : StableUnderSpecialization (range f)) : SpecializingMap f
Full source 
lemma Topology.IsInducing.specializingMap (hf : IsInducing f)
    (h : StableUnderSpecialization (range f)) : SpecializingMap f := by
  intros x y e
  obtain ⟨y, rfl⟩ := h e ⟨x, rfl⟩
  exact ⟨_, hf.specializes_iff.mp e, rfl⟩
Inducing Maps with Stable Range are Specializing
Informal description
Let $f \colon X \to Y$ be an inducing map between topological spaces. If the range of $f$ is stable under specialization, then $f$ is a specializing map.
Topology.IsInducing.generalizingMap theorem
(hf : IsInducing f) (h : StableUnderGeneralization (range f)) : GeneralizingMap f
Full source 
lemma Topology.IsInducing.generalizingMap (hf : IsInducing f)
    (h : StableUnderGeneralization (range f)) : GeneralizingMap f := by
  intros x y e
  obtain ⟨y, rfl⟩ := h e ⟨x, rfl⟩
  exact ⟨_, hf.specializes_iff.mp e, rfl⟩
Inducing Maps with Range Stable Under Generalization are Generalizing
Informal description
Let $f \colon X \to Y$ be an inducing map between topological spaces. If the range of $f$ is stable under generalization, then $f$ is a generalizing map.
IsOpenEmbedding.generalizingMap theorem
(hf : IsOpenEmbedding f) : GeneralizingMap f
Full source 
lemma IsOpenEmbedding.generalizingMap (hf : IsOpenEmbedding f) : GeneralizingMap f :=
  hf.isInducing.generalizingMap hf.isOpen_range.stableUnderGeneralization
Open embeddings are generalizing maps
Informal description
If $f \colon X \to Y$ is an open embedding between topological spaces, then $f$ is a generalizing map. That is, for any point $x' \in X$ and any point $y \in Y$ such that $y$ specializes to $f(x')$, there exists a point $x \in X$ specializing to $x'$ with $f(x) = y$.
SpecializingMap.stableUnderSpecialization_range theorem
(h : SpecializingMap f) : StableUnderSpecialization (range f)
Full source 
lemma SpecializingMap.stableUnderSpecialization_range (h : SpecializingMap f) :
    StableUnderSpecialization (range f) :=
  @image_univ _ _ f ▸ stableUnderSpecialization_univ.image h
Range of a Specializing Map is Stable Under Specialization
Informal description
If $f \colon X \to Y$ is a specializing map between topological spaces, then the range of $f$ is stable under specialization. That is, for any points $y, y' \in Y$ such that $y$ specializes to $y'$ (denoted $y \rightsquigarrow y'$) and $y$ is in the range of $f$, then $y'$ is also in the range of $f$.
GeneralizingMap.stableUnderGeneralization_image theorem
(hf : GeneralizingMap f) {s : Set X} (hs : StableUnderGeneralization s) : StableUnderGeneralization (f '' s)
Full source 
lemma GeneralizingMap.stableUnderGeneralization_image (hf : GeneralizingMap f) {s : Set X}
    (hs : StableUnderGeneralization s) : StableUnderGeneralization (f '' s) :=
  IsUpperSet.image_fibration hf hs
Image of a generalization-stable set under a generalizing map is generalization-stable
Informal description
Let $f \colon X \to Y$ be a generalizing map between topological spaces and let $s \subseteq X$ be a subset that is stable under generalization. Then the image $f(s) \subseteq Y$ is also stable under generalization.
GeneralizingMap_iff_stableUnderGeneralization_image theorem
: GeneralizingMap f ↔ ∀ s, StableUnderGeneralization s → StableUnderGeneralization (f '' s)
Full source 
lemma GeneralizingMap_iff_stableUnderGeneralization_image :
    GeneralizingMapGeneralizingMap f ↔ ∀ s, StableUnderGeneralization s → StableUnderGeneralization (f '' s) :=
  Relation.fibration_iff_isUpperSet_image
Characterization of Generalizing Maps via Preservation of Generalization-Stable Sets
Informal description
A function $f \colon X \to Y$ between topological spaces is a generalizing map if and only if for every subset $s \subseteq X$ that is stable under generalization, the image $f(s) \subseteq Y$ is also stable under generalization.
GeneralizingMap.stableUnderGeneralization_range theorem
(h : GeneralizingMap f) : StableUnderGeneralization (range f)
Full source 
lemma GeneralizingMap.stableUnderGeneralization_range (h : GeneralizingMap f) :
    StableUnderGeneralization (range f) :=
  @image_univ _ _ f ▸ stableUnderGeneralization_univ.image h
Range of a Generalizing Map is Stable Under Generalization
Informal description
If $f \colon X \to Y$ is a generalizing map between topological spaces, then the range of $f$ is stable under generalization. That is, for any points $y, y' \in Y$ such that $y$ specializes to $y'$ (i.e., $\mathcal{N}(y) \leq \mathcal{N}(y')$), if $y'$ is in the range of $f$, then $y$ is also in the range of $f$.
GeneralizingMap.comp theorem
{f : X → Y} {g : Y → Z} (hf : GeneralizingMap f) (hg : GeneralizingMap g) : GeneralizingMap (g ∘ f)
Full source 
lemma GeneralizingMap.comp {f : X → Y} {g : Y → Z}
    (hf : GeneralizingMap f) (hg : GeneralizingMap g) :
    GeneralizingMap (g ∘ f) := by
  simp only [GeneralizingMap_iff_stableUnderGeneralization_image, Set.image_comp] at *
  exact fun s h ↦ hg _ (hf  _ h)
Composition of Generalizing Maps is Generalizing
Informal description
Let $f \colon X \to Y$ and $g \colon Y \to Z$ be generalizing maps between topological spaces. Then the composition $g \circ f \colon X \to Z$ is also a generalizing map.
inseparable_def theorem
: (x ~ᵢ y) ↔ 𝓝 x = 𝓝 y
Full source 
theorem inseparable_def : (x ~ᵢ y) ↔ 𝓝 x = 𝓝 y :=
  Iff.rfl
Characterization of Inseparable Points via Neighborhood Filters
Informal description
Two points $x$ and $y$ in a topological space are inseparable if and only if their neighborhood filters $\mathcal{N}(x)$ and $\mathcal{N}(y)$ are equal, i.e., $x \sim_i y \leftrightarrow \mathcal{N}(x) = \mathcal{N}(y)$.
inseparable_iff_specializes_and theorem
: (x ~ᵢ y) ↔ x ⤳ y ∧ y ⤳ x
Full source 
theorem inseparable_iff_specializes_and : (x ~ᵢ y) ↔ x ⤳ y ∧ y ⤳ x :=
  le_antisymm_iff
Inseparability is equivalent to mutual specialization
Informal description
Two points $x$ and $y$ in a topological space are inseparable (denoted $x \sim_i y$) if and only if each specializes to the other, i.e., $x \rightsquigarrow y$ and $y \rightsquigarrow x$.
Inseparable.specializes theorem
(h : x ~ᵢ y) : x ⤳ y
Full source 
theorem Inseparable.specializes (h : x ~ᵢ y) : x ⤳ y := h.le
Inseparable Points Specialize to Each Other
Informal description
If two points $x$ and $y$ in a topological space are inseparable (denoted $x \sim_i y$), then $x$ specializes to $y$ (denoted $x \leadsto y$), meaning every neighborhood of $x$ contains $y$.
Inseparable.specializes' theorem
(h : x ~ᵢ y) : y ⤳ x
Full source 
theorem Inseparable.specializes' (h : x ~ᵢ y) : y ⤳ x := h.ge
Inseparability Implies Specialization in Both Directions
Informal description
If two points $x$ and $y$ in a topological space $X$ are inseparable (denoted $x \sim_i y$), then $y$ specializes to $x$ (denoted $y \leadsto x$), meaning that every neighborhood of $y$ is also a neighborhood of $x$.
Specializes.antisymm theorem
(h₁ : x ⤳ y) (h₂ : y ⤳ x) : x ~ᵢ y
Full source 
theorem Specializes.antisymm (h₁ : x ⤳ y) (h₂ : y ⤳ x) : x ~ᵢ y :=
  le_antisymm h₁ h₂
Antisymmetry of Specialization Implies Inseparability
Informal description
For any two points $x$ and $y$ in a topological space $X$, if $x$ specializes to $y$ (i.e., every neighborhood of $x$ contains $y$) and $y$ specializes to $x$ (i.e., every neighborhood of $y$ contains $x$), then $x$ and $y$ are inseparable (i.e., they have identical neighborhoods).
inseparable_iff_forall_isOpen theorem
: (x ~ᵢ y) ↔ ∀ s : Set X, IsOpen s → (x ∈ s ↔ y ∈ s)
Full source 
theorem inseparable_iff_forall_isOpen : (x ~ᵢ y) ↔ ∀ s : Set X, IsOpen s → (x ∈ s ↔ y ∈ s) := by
  simp only [inseparable_iff_specializes_and, specializes_iff_forall_open, ← forall_and, ← iff_def,
    Iff.comm]
Characterization of Inseparable Points via Open Sets
Informal description
Two points $x$ and $y$ in a topological space $X$ are inseparable (denoted $x \sim_i y$) if and only if for every open set $s \subseteq X$, $x$ belongs to $s$ if and only if $y$ belongs to $s$.
not_inseparable_iff_exists_open theorem
: ¬(x ~ᵢ y) ↔ ∃ s : Set X, IsOpen s ∧ Xor' (x ∈ s) (y ∈ s)
Full source 
theorem not_inseparable_iff_exists_open :
    ¬(x ~ᵢ y)¬(x ~ᵢ y) ↔ ∃ s : Set X, IsOpen s ∧ Xor' (x ∈ s) (y ∈ s) := by
  simp [inseparable_iff_forall_isOpen, ← xor_iff_not_iff]
Characterization of Non-Inseparable Points via Open Sets
Informal description
Two points $x$ and $y$ in a topological space $X$ are not inseparable if and only if there exists an open set $s \subseteq X$ such that exactly one of $x$ or $y$ belongs to $s$.
inseparable_iff_forall_isClosed theorem
: (x ~ᵢ y) ↔ ∀ s : Set X, IsClosed s → (x ∈ s ↔ y ∈ s)
Full source 
theorem inseparable_iff_forall_isClosed : (x ~ᵢ y) ↔ ∀ s : Set X, IsClosed s → (x ∈ s ↔ y ∈ s) := by
  simp only [inseparable_iff_specializes_and, specializes_iff_forall_closed, ← forall_and, ←
    iff_def]
Characterization of Inseparable Points via Closed Sets
Informal description
Two points $x$ and $y$ in a topological space $X$ are inseparable (denoted $x \sim_i y$) if and only if for every closed subset $s \subseteq X$, $x$ belongs to $s$ if and only if $y$ belongs to $s$.
inseparable_iff_mem_closure theorem
: (x ~ᵢ y) ↔ x ∈ closure ({ y } : Set X) ∧ y ∈ closure ({ x } : Set X)
Full source 
theorem inseparable_iff_mem_closure :
    (x ~ᵢ y) ↔ x ∈ closure ({y} : Set X) ∧ y ∈ closure ({x} : Set X) :=
  inseparable_iff_specializes_and.trans <| by simp only [specializes_iff_mem_closure, and_comm]
Inseparability via Mutual Closure Membership
Informal description
Two points $x$ and $y$ in a topological space $X$ are inseparable (denoted $x \sim_i y$) if and only if $x$ belongs to the closure of $\{y\}$ and $y$ belongs to the closure of $\{x\}$.
inseparable_iff_closure_eq theorem
: (x ~ᵢ y) ↔ closure ({ x } : Set X) = closure { y }
Full source 
theorem inseparable_iff_closure_eq : (x ~ᵢ y) ↔ closure ({x} : Set X) = closure {y} := by
  simp only [inseparable_iff_specializes_and, specializes_iff_closure_subset, ← subset_antisymm_iff,
    eq_comm]
Inseparability via Equality of Singleton Closures
Informal description
Two points $x$ and $y$ in a topological space $X$ are inseparable (denoted $x \sim_i y$) if and only if the closure of the singleton set $\{x\}$ is equal to the closure of the singleton set $\{y\}$.
inseparable_of_nhdsWithin_eq theorem
(hx : x ∈ s) (hy : y ∈ s) (h : 𝓝[s] x = 𝓝[s] y) : x ~ᵢ y
Full source 
theorem inseparable_of_nhdsWithin_eq (hx : x ∈ s) (hy : y ∈ s) (h : 𝓝[s] x = 𝓝[s] y) : x ~ᵢ y :=
  (specializes_of_nhdsWithin h.le hx).antisymm (specializes_of_nhdsWithin h.ge hy)
Equality of Neighborhood Filters within a Subset Implies Inseparability
Informal description
For any subset $s$ of a topological space $X$ and points $x, y \in s$, if the neighborhood filters of $x$ and $y$ within $s$ are equal (i.e., $\mathcal{N}_s(x) = \mathcal{N}_s(y)$), then $x$ and $y$ are inseparable (i.e., $x \sim_i y$).
Topology.IsInducing.inseparable_iff theorem
(hf : IsInducing f) : (f x ~ᵢ f y) ↔ (x ~ᵢ y)
Full source 
theorem Topology.IsInducing.inseparable_iff (hf : IsInducing f) : (f x ~ᵢ f y) ↔ (x ~ᵢ y) := by
  simp only [inseparable_iff_specializes_and, hf.specializes_iff]
Inseparability under Inducing Maps
Informal description
Let $f : X \to Y$ be an inducing map between topological spaces. For any points $x, y \in X$, the images $f(x)$ and $f(y)$ are inseparable in $Y$ if and only if $x$ and $y$ are inseparable in $X$.
subtype_inseparable_iff theorem
{p : X → Prop} (x y : Subtype p) : (x ~ᵢ y) ↔ ((x : X) ~ᵢ y)
Full source 
theorem subtype_inseparable_iff {p : X → Prop} (x y : Subtype p) : (x ~ᵢ y) ↔ ((x : X) ~ᵢ y) :=
  IsInducing.subtypeVal.inseparable_iff.symm
Inseparability in Subspace iff Inseparability in Ambient Space
Informal description
For any predicate $p$ on a topological space $X$ and any two points $x, y$ in the subtype defined by $p$, the points $x$ and $y$ are inseparable in the subspace topology if and only if their underlying points in $X$ are inseparable.
inseparable_prod theorem
{x₁ x₂ : X} {y₁ y₂ : Y} : ((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂)
Full source 
@[simp] theorem inseparable_prod {x₁ x₂ : X} {y₁ y₂ : Y} :
    ((x₁, y₁) ~ᵢ (x₂, y₂)) ↔ (x₁ ~ᵢ x₂) ∧ (y₁ ~ᵢ y₂) := by
  simp only [Inseparable, nhds_prod_eq, prod_inj]
Inseparability in Product Space is Component-wise Inseparability
Informal description
For any points $x_1, x_2$ in a topological space $X$ and any points $y_1, y_2$ in a topological space $Y$, the pairs $(x_1, y_1)$ and $(x_2, y_2)$ are inseparable in the product space $X \times Y$ if and only if $x_1$ is inseparable from $x_2$ in $X$ and $y_1$ is inseparable from $y_2$ in $Y$.
Inseparable.prod theorem
{x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ ~ᵢ x₂) (hy : y₁ ~ᵢ y₂) : (x₁, y₁) ~ᵢ (x₂, y₂)
Full source 
theorem Inseparable.prod {x₁ x₂ : X} {y₁ y₂ : Y} (hx : x₁ ~ᵢ x₂) (hy : y₁ ~ᵢ y₂) :
    (x₁, y₁)(x₁, y₁) ~ᵢ (x₂, y₂) :=
  inseparable_prod.2 ⟨hx, hy⟩
Inseparability is Preserved Under Products
Informal description
For any points $x_1, x_2$ in a topological space $X$ and any points $y_1, y_2$ in a topological space $Y$, if $x_1$ is inseparable from $x_2$ in $X$ and $y_1$ is inseparable from $y_2$ in $Y$, then the pairs $(x_1, y_1)$ and $(x_2, y_2)$ are inseparable in the product space $X \times Y$.
inseparable_pi theorem
{f g : ∀ i, π i} : (f ~ᵢ g) ↔ ∀ i, f i ~ᵢ g i
Full source 
@[simp]
theorem inseparable_pi {f g : ∀ i, π i} : (f ~ᵢ g) ↔ ∀ i, f i ~ᵢ g i := by
  simp only [Inseparable, nhds_pi, funext_iff, pi_inj]
Inseparability in Product Spaces is Componentwise
Informal description
For any two functions $f, g \colon \prod_{i \in \iota} \pi_i$ in a product space, $f$ and $g$ are inseparable (denoted $f \sim_i g$) if and only if for every index $i$, the components $f(i)$ and $g(i)$ are inseparable in their respective spaces $\pi_i$.
Inseparable.refl theorem
(x : X) : x ~ᵢ x
Full source 
@[refl]
theorem refl (x : X) : x ~ᵢ x :=
  Eq.refl (𝓝 x)
Reflexivity of Inseparability Relation
Informal description
For any point $x$ in a topological space $X$, the relation $x \sim_i x$ holds, meaning $x$ is inseparable from itself.
Inseparable.rfl theorem
: x ~ᵢ x
Full source 
theorem rfl : x ~ᵢ x :=
  refl x
Reflexivity of Inseparability Relation
Informal description
For any point $x$ in a topological space, $x$ is inseparable from itself, i.e., $x \sim_i x$.
Inseparable.of_eq theorem
(e : x = y) : Inseparable x y
Full source 
theorem of_eq (e : x = y) : Inseparable x y :=
  e ▸ refl x
Equality Implies Inseparability in Topological Spaces
Informal description
For any two points $x$ and $y$ in a topological space, if $x = y$, then $x$ is inseparable from $y$.
Inseparable.symm theorem
(h : x ~ᵢ y) : y ~ᵢ x
Full source 
@[symm]
nonrec theorem symm (h : x ~ᵢ y) : y ~ᵢ x := h.symm
Symmetry of Inseparability Relation in Topological Spaces
Informal description
For any two points $x$ and $y$ in a topological space, if $x$ is inseparable from $y$ (denoted $x \sim_i y$), then $y$ is inseparable from $x$ (denoted $y \sim_i x$).
Inseparable.trans theorem
(h₁ : x ~ᵢ y) (h₂ : y ~ᵢ z) : x ~ᵢ z
Full source 
@[trans]
nonrec theorem trans (h₁ : x ~ᵢ y) (h₂ : y ~ᵢ z) : x ~ᵢ z := h₁.trans h₂
Transitivity of Inseparability in Topological Spaces
Informal description
For any three points $x$, $y$, and $z$ in a topological space, if $x$ is inseparable from $y$ and $y$ is inseparable from $z$, then $x$ is inseparable from $z$.
Inseparable.nhds_eq theorem
(h : x ~ᵢ y) : 𝓝 x = 𝓝 y
Full source 
theorem nhds_eq (h : x ~ᵢ y) : 𝓝 x = 𝓝 y := h
Inseparable Points Have Equal Neighborhood Filters
Informal description
If two points $x$ and $y$ in a topological space are inseparable (denoted $x \sim_i y$), then their neighborhood filters are equal, i.e., $\mathcal{N}(x) = \mathcal{N}(y)$.
Inseparable.mem_open_iff theorem
(h : x ~ᵢ y) (hs : IsOpen s) : x ∈ s ↔ y ∈ s
Full source 
theorem mem_open_iff (h : x ~ᵢ y) (hs : IsOpen s) : x ∈ sx ∈ s ↔ y ∈ s :=
  inseparable_iff_forall_isOpen.1 h s hs
Inseparable Points Have Identical Membership in Open Sets
Informal description
For any two inseparable points $x$ and $y$ in a topological space $X$ (denoted $x \sim_i y$) and any open subset $s \subseteq X$, $x$ belongs to $s$ if and only if $y$ belongs to $s$.
Inseparable.mem_closed_iff theorem
(h : x ~ᵢ y) (hs : IsClosed s) : x ∈ s ↔ y ∈ s
Full source 
theorem mem_closed_iff (h : x ~ᵢ y) (hs : IsClosed s) : x ∈ sx ∈ s ↔ y ∈ s :=
  inseparable_iff_forall_isClosed.1 h s hs
Inseparable Points Have Identical Membership in Closed Sets
Informal description
For any two inseparable points $x$ and $y$ in a topological space $X$ (denoted $x \sim_i y$) and any closed subset $s \subseteq X$, $x$ belongs to $s$ if and only if $y$ belongs to $s$.
Inseparable.map_of_continuousAt theorem
(h : x ~ᵢ y) (hx : ContinuousAt f x) (hy : ContinuousAt f y) : f x ~ᵢ f y
Full source 
theorem map_of_continuousAt (h : x ~ᵢ y) (hx : ContinuousAt f x) (hy : ContinuousAt f y) :
    f x ~ᵢ f y :=
  (h.specializes.map_of_continuousAt hy).antisymm (h.specializes'.map_of_continuousAt hx)
Continuous Functions Preserve Inseparability at Points
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a function, and $x, y \in X$. If $x$ and $y$ are inseparable (i.e., $x \sim_i y$) and $f$ is continuous at both $x$ and $y$, then $f(x)$ and $f(y)$ are inseparable in $Y$.
Inseparable.map theorem
(h : x ~ᵢ y) (hf : Continuous f) : f x ~ᵢ f y
Full source 
theorem map (h : x ~ᵢ y) (hf : Continuous f) : f x ~ᵢ f y :=
  h.map_of_continuousAt hf.continuousAt hf.continuousAt
Continuous Functions Preserve Inseparability
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y$ a continuous function, and $x, y \in X$ inseparable points (i.e., $x \sim_i y$). Then their images $f(x)$ and $f(y)$ are inseparable in $Y$.
IsClosed.not_inseparable theorem
(hs : IsClosed s) (hx : x ∈ s) (hy : y ∉ s) : ¬(x ~ᵢ y)
Full source 
theorem IsClosed.not_inseparable (hs : IsClosed s) (hx : x ∈ s) (hy : y ∉ s) : ¬(x ~ᵢ y) := fun h =>
  hy <| (h.mem_closed_iff hs).1 hx
Closed Sets Distinguish Inseparable Points
Informal description
For any closed subset $s$ of a topological space $X$, if $x \in s$ and $y \notin s$, then $x$ and $y$ are not inseparable (i.e., $x \not\sim_i y$).
IsOpen.not_inseparable theorem
(hs : IsOpen s) (hx : x ∈ s) (hy : y ∉ s) : ¬(x ~ᵢ y)
Full source 
theorem IsOpen.not_inseparable (hs : IsOpen s) (hx : x ∈ s) (hy : y ∉ s) : ¬(x ~ᵢ y) := fun h =>
  hy <| (h.mem_open_iff hs).1 hx
Open Sets Distinguish Inseparable Points
Informal description
For any open set $s$ in a topological space, if $x \in s$ and $y \notin s$, then $x$ and $y$ are not inseparable (i.e., $x \not\sim_i y$).
instTopologicalSpaceSeparationQuotient instance
: TopologicalSpace (SeparationQuotient X)
Full source 
instance : TopologicalSpace (SeparationQuotient X) := instTopologicalSpaceQuotient
Topology on the Separation Quotient
Informal description
The separation quotient of a topological space $X$, which is the quotient space obtained by identifying inseparable points in $X$, carries a natural topological space structure inherited from $X$.
SeparationQuotient.mk definition
: X → SeparationQuotient X
Full source 
/-- The natural map from a topological space to its separation quotient. -/
def mk : X → SeparationQuotient X := Quotient.mk''
Separation quotient projection map
Informal description
The natural projection map from a topological space $X$ to its separation quotient, which is the quotient space obtained by identifying inseparable points in $X$.
SeparationQuotient.isQuotientMap_mk theorem
: IsQuotientMap (mk : X → SeparationQuotient X)
Full source 
theorem isQuotientMap_mk : IsQuotientMap (mk : X → SeparationQuotient X) :=
  isQuotientMap_quot_mk
Quotient Map Property of the Separation Quotient Projection
Informal description
The natural projection map $\operatorname{mk} : X \to \operatorname{SeparationQuotient} X$ is a quotient map, meaning it is continuous, surjective, and the topology on $\operatorname{SeparationQuotient} X$ is the finest topology for which this map is continuous.
SeparationQuotient.continuous_mk theorem
: Continuous (mk : X → SeparationQuotient X)
Full source 
@[fun_prop, continuity]
theorem continuous_mk : Continuous (mk : X → SeparationQuotient X) :=
  continuous_quot_mk
Continuity of the Separation Quotient Projection
Informal description
The natural projection map $\operatorname{mk} : X \to \operatorname{SeparationQuotient} X$ is continuous, where $\operatorname{SeparationQuotient} X$ is the quotient space obtained by identifying inseparable points in the topological space $X$.
SeparationQuotient.mk_eq_mk theorem
: mk x = mk y ↔ (x ~ᵢ y)
Full source 
@[simp]
theorem mk_eq_mk : mkmk x = mk y ↔ (x ~ᵢ y) :=
  Quotient.eq''
Separation Quotient Equality Criterion via Inseparability
Informal description
For any two points $x$ and $y$ in a topological space $X$, the images of $x$ and $y$ under the separation quotient projection map are equal if and only if $x$ and $y$ are inseparable (i.e., they have the same neighborhood filters). In symbols: $$\operatorname{mk}(x) = \operatorname{mk}(y) \leftrightarrow x \sim_i y$$
SeparationQuotient.surjective_mk theorem
: Surjective (mk : X → SeparationQuotient X)
Full source 
theorem surjective_mk : Surjective (mk : X → SeparationQuotient X) :=
  Quot.mk_surjective
Surjectivity of the Separation Quotient Projection
Informal description
The natural projection map $\operatorname{mk} : X \to \operatorname{SeparationQuotient} X$ is surjective. That is, for every element $q$ in the separation quotient of $X$, there exists a point $x \in X$ such that $\operatorname{mk}(x) = q$.
SeparationQuotient.range_mk theorem
: range (mk : X → SeparationQuotient X) = univ
Full source 
@[simp]
theorem range_mk : range (mk : X → SeparationQuotient X) = univ :=
  surjective_mk.range_eq
Range of Separation Quotient Projection is Universal Set
Informal description
The range of the projection map $\operatorname{mk} : X \to \operatorname{SeparationQuotient} X$ is equal to the universal set of the separation quotient. In other words, every element of the separation quotient is the image of some point in $X$ under the projection map.
SeparationQuotient.instNonempty instance
[Nonempty X] : Nonempty (SeparationQuotient X)
Full source 
instance [Nonempty X] : Nonempty (SeparationQuotient X) :=
  Nonempty.map mk ‹_›
Nonempty Separation Quotient of Nonempty Space
Informal description
For any nonempty topological space $X$, its separation quotient $\operatorname{SeparationQuotient} X$ is also nonempty.
SeparationQuotient.instInhabited instance
[Inhabited X] : Inhabited (SeparationQuotient X)
Full source 
instance [Inhabited X] : Inhabited (SeparationQuotient X) :=
  ⟨mk default⟩
Inhabited Separation Quotient of Inhabited Space
Informal description
For any inhabited topological space $X$, its separation quotient $\operatorname{SeparationQuotient} X$ is also inhabited.
SeparationQuotient.instSubsingleton instance
[Subsingleton X] : Subsingleton (SeparationQuotient X)
Full source 
instance [Subsingleton X] : Subsingleton (SeparationQuotient X) :=
  surjective_mk.subsingleton
Subsingleton Property of Separation Quotient for Subsingleton Spaces
Informal description
For any topological space $X$ that is a subsingleton (i.e., all points are equal), its separation quotient $\operatorname{SeparationQuotient} X$ is also a subsingleton.
SeparationQuotient.instOne instance
[One X] : One (SeparationQuotient X)
Full source 
@[to_additive] instance [One X] : One (SeparationQuotient X) := ⟨mk 1⟩
One Element in the Separation Quotient
Informal description
For any topological space $X$ with a distinguished element $1$, the separation quotient $\operatorname{SeparationQuotient} X$ inherits a distinguished element, which is the image of $1$ under the quotient map.
SeparationQuotient.mk_one theorem
[One X] : mk (1 : X) = 1
Full source 
@[to_additive (attr := simp)] theorem mk_one [One X] : mk (1 : X) = 1 := rfl
Preservation of Identity in Separation Quotient
Informal description
For any topological space $X$ with a distinguished element $1$, the image of $1$ under the separation quotient map $\operatorname{SeparationQuotient} X$ is equal to the distinguished element in the quotient space.
SeparationQuotient.preimage_image_mk_open theorem
(hs : IsOpen s) : mk ⁻¹' (mk '' s) = s
Full source 
theorem preimage_image_mk_open (hs : IsOpen s) : mkmk ⁻¹' (mk '' s) = s := by
  refine Subset.antisymm ?_ (subset_preimage_image _ _)
  rintro x ⟨y, hys, hxy⟩
  exact ((mk_eq_mk.1 hxy).mem_open_iff hs).1 hys
Preimage of Image Equals Original Set for Open Sets under Separation Quotient Map
Informal description
For any open subset $s$ of a topological space $X$, the preimage under the separation quotient map $\operatorname{mk} : X \to \operatorname{SeparationQuotient} X$ of the image of $s$ is equal to $s$ itself. In symbols: $$\operatorname{mk}^{-1}(\operatorname{mk}(s)) = s$$
SeparationQuotient.isOpenMap_mk theorem
: IsOpenMap (mk : X → SeparationQuotient X)
Full source 
theorem isOpenMap_mk : IsOpenMap (mk : X → SeparationQuotient X) := fun s hs =>
  isQuotientMap_mk.isOpen_preimage.1 <| by rwa [preimage_image_mk_open hs]
Open Map Property of the Separation Quotient Projection
Informal description
The natural projection map $\operatorname{mk} \colon X \to \operatorname{SeparationQuotient} X$ is an open map, meaning that for every open set $U \subseteq X$, its image $\operatorname{mk}(U)$ is open in the separation quotient.
SeparationQuotient.isOpenQuotientMap_mk theorem
: IsOpenQuotientMap (mk : X → SeparationQuotient X)
Full source 
theorem isOpenQuotientMap_mk : IsOpenQuotientMap (mk : X → SeparationQuotient X) :=
  ⟨surjective_mk, continuous_mk, isOpenMap_mk⟩
Open Quotient Map Property of the Separation Quotient Projection
Informal description
The natural projection map $\operatorname{mk} \colon X \to \operatorname{SeparationQuotient} X$ is an open quotient map, meaning it is both an open map and a quotient map.
SeparationQuotient.preimage_image_mk_closed theorem
(hs : IsClosed s) : mk ⁻¹' (mk '' s) = s
Full source 
theorem preimage_image_mk_closed (hs : IsClosed s) : mkmk ⁻¹' (mk '' s) = s := by
  refine Subset.antisymm ?_ (subset_preimage_image _ _)
  rintro x ⟨y, hys, hxy⟩
  exact ((mk_eq_mk.1 hxy).mem_closed_iff hs).1 hys
Preimage of Image Equals Original Set for Closed Sets under Separation Quotient
Informal description
For any closed subset $s$ of a topological space $X$, the preimage under the separation quotient projection $\operatorname{mk} : X \to \operatorname{SeparationQuotient} X$ of the image of $s$ equals $s$ itself. In symbols: $$\operatorname{mk}^{-1}(\operatorname{mk}(s)) = s$$
SeparationQuotient.isInducing_mk theorem
: IsInducing (mk : X → SeparationQuotient X)
Full source 
theorem isInducing_mk : IsInducing (mk : X → SeparationQuotient X) :=
  ⟨le_antisymm (continuous_iff_le_induced.1 continuous_mk) fun s hs =>
      ⟨mk '' s, isOpenMap_mk s hs, preimage_image_mk_open hs⟩⟩
Inducing Property of the Separation Quotient Projection
Informal description
The natural projection map $\operatorname{mk} \colon X \to \operatorname{SeparationQuotient} X$ is inducing, meaning that the topology on the separation quotient is the finest topology for which $\operatorname{mk}$ is continuous. In other words, a set in the separation quotient is open if and only if its preimage under $\operatorname{mk}$ is open in $X$.
SeparationQuotient.isClosedMap_mk theorem
: IsClosedMap (mk : X → SeparationQuotient X)
Full source 
theorem isClosedMap_mk : IsClosedMap (mk : X → SeparationQuotient X) :=
  isInducing_mk.isClosedMap <| by rw [range_mk]; exact isClosed_univ
Projection to Separation Quotient is a Closed Map
Informal description
The natural projection map $\operatorname{mk} \colon X \to \operatorname{SeparationQuotient} X$ is a closed map, meaning that the image of any closed subset of $X$ under $\operatorname{mk}$ is closed in the separation quotient.
SeparationQuotient.comap_mk_nhds_mk theorem
: comap mk (𝓝 (mk x)) = 𝓝 x
Full source 
@[simp]
theorem comap_mk_nhds_mk : comap mk (𝓝 (mk x)) = 𝓝 x :=
  (isInducing_mk.nhds_eq_comap _).symm
Neighborhood Filter Preservation under Separation Quotient Projection
Informal description
For any point $x$ in a topological space $X$, the preimage under the separation quotient projection $\operatorname{mk} \colon X \to \operatorname{SeparationQuotient} X$ of the neighborhood filter of $\operatorname{mk}(x)$ in the separation quotient is equal to the neighborhood filter of $x$ in $X$, i.e., \[ \operatorname{mk}^{-1}(\mathcal{N}(\operatorname{mk}(x))) = \mathcal{N}(x). \]
SeparationQuotient.comap_mk_nhdsSet_image theorem
: comap mk (𝓝ˢ (mk '' s)) = 𝓝ˢ s
Full source 
@[simp]
theorem comap_mk_nhdsSet_image : comap mk (𝓝ˢ (mkmk '' s)) = 𝓝ˢ s :=
  (isInducing_mk.nhdsSet_eq_comap _).symm
Preimage of Neighborhood Filter under Separation Quotient Equals Original Neighborhood Filter
Informal description
For any subset $s$ of a topological space $X$, the preimage under the separation quotient projection $\operatorname{mk} \colon X \to \operatorname{SeparationQuotient} X$ of the neighborhood filter of the image $\operatorname{mk}(s)$ in the separation quotient equals the neighborhood filter of $s$ in $X$. In symbols: $$\operatorname{mk}^{-1}(\mathcal{N}(\operatorname{mk}(s))) = \mathcal{N}(s).$$
SeparationQuotient.map_mk_nhds theorem
: map mk (𝓝 x) = 𝓝 (mk x)
Full source 
/-- Push-forward of the neighborhood of a point along the projection to the separation quotient
is the neighborhood of its equivalence class. -/
theorem map_mk_nhds : map mk (𝓝 x) = 𝓝 (mk x) := by
  rw [← comap_mk_nhds_mk, map_comap_of_surjective surjective_mk]
Neighborhood Filter Pushforward under Separation Quotient Projection
Informal description
For any point $x$ in a topological space $X$, the pushforward of the neighborhood filter $\mathcal{N}(x)$ under the separation quotient projection $\operatorname{mk} \colon X \to \operatorname{SeparationQuotient} X$ equals the neighborhood filter of $\operatorname{mk}(x)$ in the separation quotient, i.e., \[ \operatorname{mk}_*(\mathcal{N}(x)) = \mathcal{N}(\operatorname{mk}(x)). \]
SeparationQuotient.nhds_mk theorem
(x : X) : 𝓝 (mk x) = .map mk (𝓝 x)
Full source 
@[deprecated map_mk_nhds (since := "2025-03-21")]
theorem nhds_mk (x : X) : 𝓝 (mk x) = .map mk (𝓝 x) := .symm <| map_mk_nhds ..
Neighborhood Filter Preservation under Separation Quotient Projection
Informal description
For any point $x$ in a topological space $X$, the neighborhood filter of the image of $x$ under the separation quotient projection $\operatorname{mk} \colon X \to \operatorname{SeparationQuotient} X$ is equal to the pushforward of the neighborhood filter of $x$ under $\operatorname{mk}$. In symbols: \[ \mathcal{N}(\operatorname{mk}(x)) = \operatorname{mk}_*(\mathcal{N}(x)). \]
SeparationQuotient.map_mk_nhdsSet theorem
: map mk (𝓝ˢ s) = 𝓝ˢ (mk '' s)
Full source 
theorem map_mk_nhdsSet : map mk (𝓝ˢ s) = 𝓝ˢ (mkmk '' s) := by
  rw [← comap_mk_nhdsSet_image, map_comap_of_surjective surjective_mk]
Image of Neighborhood Filter under Separation Quotient Equals Neighborhood Filter of Image
Informal description
For any subset $s$ of a topological space $X$, the image under the separation quotient projection $\operatorname{mk} \colon X \to \operatorname{SeparationQuotient} X$ of the neighborhood filter of $s$ equals the neighborhood filter of the image $\operatorname{mk}(s)$ in the separation quotient. In symbols: $$\operatorname{mk}_*(\mathcal{N}(s)) = \mathcal{N}(\operatorname{mk}(s)).$$
SeparationQuotient.comap_mk_nhdsSet theorem
: comap mk (𝓝ˢ t) = 𝓝ˢ (mk ⁻¹' t)
Full source 
theorem comap_mk_nhdsSet : comap mk (𝓝ˢ t) = 𝓝ˢ (mkmk ⁻¹' t) := by
  conv_lhs => rw [← image_preimage_eq t surjective_mk, comap_mk_nhdsSet_image]
Preimage of Neighborhood Filter Equals Neighborhood Filter of Preimage in Separation Quotient
Informal description
For any subset $t$ of the separation quotient $\operatorname{SeparationQuotient} X$, the preimage under the projection map $\operatorname{mk}$ of the neighborhood filter of $t$ equals the neighborhood filter of the preimage of $t$ in $X$. In symbols: $$\operatorname{mk}^{-1}(\mathcal{N}(t)) = \mathcal{N}(\operatorname{mk}^{-1}(t)).$$
SeparationQuotient.preimage_mk_closure theorem
: mk ⁻¹' closure t = closure (mk ⁻¹' t)
Full source 
theorem preimage_mk_closure : mkmk ⁻¹' closure t = closure (mkmk ⁻¹' t) :=
  isOpenMap_mk.preimage_closure_eq_closure_preimage continuous_mk t
Equality of Preimage Closure and Closure Preimage in Separation Quotient
Informal description
For any subset $t$ of the separation quotient $\operatorname{SeparationQuotient} X$, the preimage under the projection map $\operatorname{mk}$ of the closure of $t$ equals the closure of the preimage of $t$, i.e., \[ \operatorname{mk}^{-1}(\overline{t}) = \overline{\operatorname{mk}^{-1}(t)}. \]
SeparationQuotient.preimage_mk_interior theorem
: mk ⁻¹' interior t = interior (mk ⁻¹' t)
Full source 
theorem preimage_mk_interior : mkmk ⁻¹' interior t = interior (mkmk ⁻¹' t) :=
  isOpenMap_mk.preimage_interior_eq_interior_preimage continuous_mk t
Equality of Preimage Interior and Interior Preimage in Separation Quotient
Informal description
For any subset $t$ of the separation quotient $\operatorname{SeparationQuotient} X$, the preimage under the projection map $\operatorname{mk}$ of the interior of $t$ equals the interior of the preimage of $t$, i.e., \[ \operatorname{mk}^{-1}(\text{int}(t)) = \text{int}(\operatorname{mk}^{-1}(t)). \]
SeparationQuotient.preimage_mk_frontier theorem
: mk ⁻¹' frontier t = frontier (mk ⁻¹' t)
Full source 
theorem preimage_mk_frontier : mkmk ⁻¹' frontier t = frontier (mkmk ⁻¹' t) :=
  isOpenMap_mk.preimage_frontier_eq_frontier_preimage continuous_mk t
Frontier Preservation in Separation Quotient Preimage
Informal description
For any subset $t$ of the separation quotient $\operatorname{SeparationQuotient} X$, the preimage under the projection map $\operatorname{mk}$ of the frontier of $t$ equals the frontier of the preimage of $t$, i.e., \[ \operatorname{mk}^{-1}(\partial t) = \partial \operatorname{mk}^{-1}(t). \]
SeparationQuotient.image_mk_closure theorem
: mk '' closure s = closure (mk '' s)
Full source 
theorem image_mk_closure : mkmk '' closure s = closure (mkmk '' s) :=
  (image_closure_subset_closure_image continuous_mk).antisymm <|
    isClosedMap_mk.closure_image_subset _
Closure Preservation under Separation Quotient Projection
Informal description
For any subset $s$ of a topological space $X$, the image of the closure of $s$ under the projection map $\operatorname{mk} \colon X \to \operatorname{SeparationQuotient} X$ equals the closure of the image of $s$ under $\operatorname{mk}$, i.e., \[ \operatorname{mk}(\overline{s}) = \overline{\operatorname{mk}(s)}. \]
SeparationQuotient.map_prod_map_mk_nhds theorem
(x : X) (y : Y) : map (Prod.map mk mk) (𝓝 (x, y)) = 𝓝 (mk x, mk y)
Full source 
theorem map_prod_map_mk_nhds (x : X) (y : Y) :
    map (Prod.map mk mk) (𝓝 (x, y)) = 𝓝 (mk x, mk y) := by
  rw [nhds_prod_eq, ← prod_map_map_eq', map_mk_nhds, map_mk_nhds, nhds_prod_eq]
Neighborhood Filter Preservation under Product of Separation Quotient Projections
Informal description
For any points $x$ in a topological space $X$ and $y$ in a topological space $Y$, the pushforward of the neighborhood filter $\mathcal{N}((x,y))$ under the product map $\operatorname{mk} \times \operatorname{mk} \colon X \times Y \to \operatorname{SeparationQuotient} X \times \operatorname{SeparationQuotient} Y$ equals the neighborhood filter of $(\operatorname{mk}(x), \operatorname{mk}(y))$ in the product space, i.e., \[ (\operatorname{mk} \times \operatorname{mk})_*(\mathcal{N}((x,y))) = \mathcal{N}((\operatorname{mk}(x), \operatorname{mk}(y))). \]
SeparationQuotient.map_mk_nhdsWithin_preimage theorem
(s : Set (SeparationQuotient X)) (x : X) : map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x
Full source 
theorem map_mk_nhdsWithin_preimage (s : Set (SeparationQuotient X)) (x : X) :
    map mk (𝓝[mk ⁻¹' s] x) = 𝓝[s] mk x := by
  rw [nhdsWithin, ← comap_principal, Filter.push_pull, nhdsWithin, map_mk_nhds]
Neighborhood Filter Pushforward under Separation Quotient Projection with Preimage Restriction
Informal description
For any subset $s$ of the separation quotient $\operatorname{SeparationQuotient} X$ and any point $x \in X$, the pushforward under the projection map $\operatorname{mk} \colon X \to \operatorname{SeparationQuotient} X$ of the neighborhood filter of $x$ restricted to the preimage $\operatorname{mk}^{-1}(s)$ equals the neighborhood filter of $\operatorname{mk}(x)$ restricted to $s$. In symbols: \[ \operatorname{mk}_*(\mathcal{N}_{\operatorname{mk}^{-1}(s)}(x)) = \mathcal{N}_s(\operatorname{mk}(x)). \]
SeparationQuotient.isQuotientMap_prodMap_mk theorem
: IsQuotientMap (Prod.map mk mk : X × Y → _)
Full source 
/-- The map `(x, y) ↦ (mk x, mk y)` is a quotient map. -/
theorem isQuotientMap_prodMap_mk : IsQuotientMap (Prod.map mk mk : X × Y → _) :=
  (isOpenQuotientMap_mk.prodMap isOpenQuotientMap_mk).isQuotientMap
Quotient Map Property of the Product of Separation Quotient Projections
Informal description
The product map $\operatorname{Prod.map} \operatorname{mk} \operatorname{mk} \colon X \times Y \to \operatorname{SeparationQuotient} X \times \operatorname{SeparationQuotient} Y$, where $\operatorname{mk}$ is the projection to the separation quotient, is a quotient map.
SeparationQuotient.lift definition
(f : X → α) (hf : ∀ x y, (x ~ᵢ y) → f x = f y) : SeparationQuotient X → α
Full source 
/-- Lift a map `f : X → α` such that `Inseparable x y → f x = f y` to a map
`SeparationQuotient X → α`. -/
def lift (f : X → α) (hf : ∀ x y, (x ~ᵢ y) → f x = f y) : SeparationQuotient X → α := fun x =>
  Quotient.liftOn' x f hf
Lifting a function to the separation quotient
Informal description
Given a topological space \( X \) and a function \( f : X \to \alpha \) that respects the inseparable relation (i.e., \( f(x) = f(y) \) whenever \( x \) and \( y \) are inseparable points in \( X \)), the function `SeparationQuotient.lift` lifts \( f \) to a function from the separation quotient \( \text{SeparationQuotient}\, X \) to \( \alpha \). Here, \( \text{SeparationQuotient}\, X \) is the quotient of \( X \) by the equivalence relation of inseparability.
SeparationQuotient.lift_mk theorem
{f : X → α} (hf : ∀ x y, (x ~ᵢ y) → f x = f y) (x : X) : lift f hf (mk x) = f x
Full source 
@[simp]
theorem lift_mk {f : X → α} (hf : ∀ x y, (x ~ᵢ y) → f x = f y) (x : X) : lift f hf (mk x) = f x :=
  rfl
Lifted Function on Separation Quotient Evaluates to Original Function
Informal description
Let $X$ be a topological space and $\alpha$ be a type. For any function $f \colon X \to \alpha$ that respects the inseparable relation (i.e., $f(x) = f(y)$ whenever $x$ and $y$ are inseparable in $X$), the lifted function $\text{lift}\, f\, hf$ evaluated at the projection $\text{mk}\, x$ of any point $x \in X$ equals $f(x)$. In other words, $\text{lift}\, f\, hf (\text{mk}\, x) = f(x)$.
SeparationQuotient.lift_comp_mk theorem
{f : X → α} (hf : ∀ x y, (x ~ᵢ y) → f x = f y) : lift f hf ∘ mk = f
Full source 
@[simp]
theorem lift_comp_mk {f : X → α} (hf : ∀ x y, (x ~ᵢ y) → f x = f y) : liftlift f hf ∘ mk = f :=
  rfl
Lifted Function Composed with Projection Equals Original Function
Informal description
For any topological space $X$ and any function $f \colon X \to \alpha$ that respects the inseparable relation (i.e., $f(x) = f(y)$ whenever $x \sim_i y$), the composition of the lifted function $\text{lift}\, f\, hf$ with the natural projection $\text{mk} \colon X \to \text{SeparationQuotient}\, X$ equals $f$. In other words, $(\text{lift}\, f\, hf) \circ \text{mk} = f$.
SeparationQuotient.tendsto_lift_nhds_mk theorem
{f : X → α} {hf : ∀ x y, (x ~ᵢ y) → f x = f y} {l : Filter α} : Tendsto (lift f hf) (𝓝 <| mk x) l ↔ Tendsto f (𝓝 x) l
Full source 
@[simp]
theorem tendsto_lift_nhds_mk {f : X → α} {hf : ∀ x y, (x ~ᵢ y) → f x = f y} {l : Filter α} :
    TendstoTendsto (lift f hf) (𝓝 <| mk x) l ↔ Tendsto f (𝓝 x) l := by
  simp only [← map_mk_nhds, tendsto_map'_iff, lift_comp_mk]
Equivalence of Filter Limits under Separation Quotient Lift
Informal description
Let $X$ be a topological space and $\alpha$ be a type. For any function $f \colon X \to \alpha$ that respects the inseparable relation (i.e., $f(x) = f(y)$ whenever $x$ and $y$ are inseparable in $X$), and for any filter $l$ on $\alpha$, the following equivalence holds: \[ \text{lift}\, f\, hf \text{ tends to } l \text{ at } \text{mk}\, x \text{ in the separation quotient} \leftrightarrow f \text{ tends to } l \text{ at } x \text{ in } X. \] Here, $\text{mk} \colon X \to \text{SeparationQuotient}\, X$ is the natural projection map, and $\text{lift}\, f\, hf$ is the lifted function on the separation quotient.
SeparationQuotient.tendsto_lift_nhdsWithin_mk theorem
{f : X → α} {hf : ∀ x y, (x ~ᵢ y) → f x = f y} {s : Set (SeparationQuotient X)} {l : Filter α} : Tendsto (lift f hf) (𝓝[s] mk x) l ↔ Tendsto f (𝓝[mk ⁻¹' s] x) l
Full source 
@[simp]
theorem tendsto_lift_nhdsWithin_mk {f : X → α} {hf : ∀ x y, (x ~ᵢ y) → f x = f y}
    {s : Set (SeparationQuotient X)} {l : Filter α} :
    TendstoTendsto (lift f hf) (𝓝[s] mk x) l ↔ Tendsto f (𝓝[mk ⁻¹' s] x) l := by
  simp only [← map_mk_nhdsWithin_preimage, tendsto_map'_iff, lift_comp_mk]
Equivalence of Filter Limits within a Set under Separation Quotient Lift
Informal description
Let $X$ be a topological space and $\alpha$ be a type. For any function $f \colon X \to \alpha$ that respects the inseparable relation (i.e., $f(x) = f(y)$ whenever $x$ and $y$ are inseparable in $X$), any subset $s$ of the separation quotient $\text{SeparationQuotient}\, X$, and any filter $l$ on $\alpha$, the following equivalence holds: \[ \text{lift}\, f\, hf \text{ tends to } l \text{ within } s \text{ at } \text{mk}\, x \leftrightarrow f \text{ tends to } l \text{ within } \text{mk}^{-1}(s) \text{ at } x. \] Here, $\text{mk} \colon X \to \text{SeparationQuotient}\, X$ is the natural projection map, and $\text{lift}\, f\, hf$ is the lifted function on the separation quotient.
SeparationQuotient.continuousAt_lift theorem
{hf : ∀ x y, (x ~ᵢ y) → f x = f y} : ContinuousAt (lift f hf) (mk x) ↔ ContinuousAt f x
Full source 
@[simp]
theorem continuousAt_lift {hf : ∀ x y, (x ~ᵢ y) → f x = f y} :
    ContinuousAtContinuousAt (lift f hf) (mk x) ↔ ContinuousAt f x :=
  tendsto_lift_nhds_mk
Continuity at a Point under Separation Quotient Lift
Informal description
Let $X$ be a topological space and $\alpha$ be a type. For any function $f \colon X \to \alpha$ that respects the inseparable relation (i.e., $f(x) = f(y)$ whenever $x$ and $y$ are inseparable in $X$), the lifted function $\text{lift}\, f\, hf$ on the separation quotient is continuous at $\text{mk}\, x$ if and only if $f$ is continuous at $x$ in $X$.
SeparationQuotient.continuousWithinAt_lift theorem
{hf : ∀ x y, (x ~ᵢ y) → f x = f y} {s : Set (SeparationQuotient X)} : ContinuousWithinAt (lift f hf) s (mk x) ↔ ContinuousWithinAt f (mk ⁻¹' s) x
Full source 
@[simp]
theorem continuousWithinAt_lift {hf : ∀ x y, (x ~ᵢ y) → f x = f y}
    {s : Set (SeparationQuotient X)} :
    ContinuousWithinAtContinuousWithinAt (lift f hf) s (mk x) ↔ ContinuousWithinAt f (mk ⁻¹' s) x :=
  tendsto_lift_nhdsWithin_mk
Continuity Within a Set at a Point under Separation Quotient Lift
Informal description
Let $X$ be a topological space and $\alpha$ be a type. For any function $f \colon X \to \alpha$ that respects the inseparable relation (i.e., $f(x) = f(y)$ whenever $x$ and $y$ are inseparable in $X$), any subset $s$ of the separation quotient $\text{SeparationQuotient}\, X$, and any point $x \in X$, the following equivalence holds: \[ \text{lift}\, f\, hf \text{ is continuous within } s \text{ at } \text{mk}\, x \leftrightarrow f \text{ is continuous within } \text{mk}^{-1}(s) \text{ at } x. \] Here, $\text{mk} \colon X \to \text{SeparationQuotient}\, X$ is the natural projection map, and $\text{lift}\, f\, hf$ is the lifted function on the separation quotient.
SeparationQuotient.continuousOn_lift theorem
{hf : ∀ x y, (x ~ᵢ y) → f x = f y} {s : Set (SeparationQuotient X)} : ContinuousOn (lift f hf) s ↔ ContinuousOn f (mk ⁻¹' s)
Full source 
@[simp]
theorem continuousOn_lift {hf : ∀ x y, (x ~ᵢ y) → f x = f y} {s : Set (SeparationQuotient X)} :
    ContinuousOnContinuousOn (lift f hf) s ↔ ContinuousOn f (mk ⁻¹' s) := by
  simp only [ContinuousOn, surjective_mk.forall, continuousWithinAt_lift, mem_preimage]
Continuity of Lifted Function on Subset of Separation Quotient
Informal description
Let $X$ be a topological space and $f \colon X \to \alpha$ a function that respects the inseparable relation (i.e., $f(x) = f(y)$ whenever $x$ and $y$ are inseparable in $X$). For any subset $s$ of the separation quotient of $X$, the lifted function $\operatorname{lift} f hf$ is continuous on $s$ if and only if $f$ is continuous on the preimage of $s$ under the quotient map $\operatorname{mk} \colon X \to \operatorname{SeparationQuotient} X$.
SeparationQuotient.continuous_lift theorem
{hf : ∀ x y, (x ~ᵢ y) → f x = f y} : Continuous (lift f hf) ↔ Continuous f
Full source 
@[simp]
theorem continuous_lift {hf : ∀ x y, (x ~ᵢ y) → f x = f y} :
    ContinuousContinuous (lift f hf) ↔ Continuous f := by
  simp only [continuous_iff_continuousOn_univ, continuousOn_lift, preimage_univ]
Continuity of Lifted Function on Separation Quotient
Informal description
For a function $f : X \to \alpha$ that respects the inseparable relation (i.e., $f(x) = f(y)$ whenever $x \sim_i y$), the lifted function $\text{lift}\, f\, hf$ on the separation quotient is continuous if and only if $f$ is continuous.
SeparationQuotient.lift₂ definition
(f : X → Y → α) (hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d) : SeparationQuotient X → SeparationQuotient Y → α
Full source 
/-- Lift a map `f : X → Y → α` such that `Inseparable a b → Inseparable c d → f a c = f b d` to a
map `SeparationQuotient X → SeparationQuotient Y → α`. -/
def lift₂ (f : X → Y → α) (hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d) :
    SeparationQuotient X → SeparationQuotient Y → α := fun x y => Quotient.liftOn₂' x y f hf
Lifting a binary function to separation quotients
Informal description
Given a topological space $X$ and a binary function $f : X \to Y \to \alpha$ that respects the inseparable relation (i.e., $f\, a\, b = f\, c\, d$ whenever $a$ and $c$ are inseparable in $X$ and $b$ and $d$ are inseparable in $Y$), the function $\text{SeparationQuotient.lift₂}\, f\, hf$ lifts $f$ to a function on the separation quotients of $X$ and $Y$. Specifically, for any $x : \text{SeparationQuotient}\, X$ and $y : \text{SeparationQuotient}\, Y$, $\text{SeparationQuotient.lift₂}\, f\, hf\, x\, y$ applies $f$ to representative elements of $x$ and $y$ in a way that is independent of the choice of representatives.
SeparationQuotient.lift₂_mk theorem
{f : X → Y → α} (hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d) (x : X) (y : Y) : lift₂ f hf (mk x) (mk y) = f x y
Full source 
@[simp]
theorem lift₂_mk {f : X → Y → α} (hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d) (x : X)
    (y : Y) : lift₂ f hf (mk x) (mk y) = f x y :=
  rfl
Lifted Binary Function on Separation Quotient Preserves Value on Representatives
Informal description
Given a binary function $f : X \to Y \to \alpha$ that respects the inseparable relation (i.e., $f(a, b) = f(c, d)$ whenever $a \sim_i c$ in $X$ and $b \sim_i d$ in $Y$), then for any points $x \in X$ and $y \in Y$, the lifted function $\text{lift}_2\, f\, hf$ applied to the projections of $x$ and $y$ in the separation quotient equals $f(x, y)$. In other words, $\text{lift}_2\, f\, hf\, (\text{mk}\, x)\, (\text{mk}\, y) = f(x, y)$.
SeparationQuotient.tendsto_lift₂_nhds theorem
{f : X → Y → α} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d} {x : X} {y : Y} {l : Filter α} : Tendsto (uncurry <| lift₂ f hf) (𝓝 (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l
Full source 
@[simp]
theorem tendsto_lift₂_nhds {f : X → Y → α} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d}
    {x : X} {y : Y} {l : Filter α} :
    TendstoTendsto (uncurry <| lift₂ f hf) (𝓝 (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝 (x, y)) l := by
  rw [← map_prod_map_mk_nhds, tendsto_map'_iff]
  rfl
Limit Preservation under Lifting to Separation Quotient
Informal description
For any binary function $f \colon X \to Y \to \alpha$ that respects the inseparable relation (i.e., $f(a, b) = f(c, d)$ whenever $a$ and $c$ are inseparable in $X$ and $b$ and $d$ are inseparable in $Y$), and for any points $x \in X$, $y \in Y$, and any filter $l$ on $\alpha$, the following are equivalent: 1. The lifted function $\operatorname{lift}_2\, f\, hf$ tends to $l$ as its argument tends to $(\operatorname{mk}(x), \operatorname{mk}(y))$ in the product space of separation quotients. 2. The original function $f$ tends to $l$ as its argument tends to $(x, y)$ in the product space $X \times Y$. In other words, the limit behavior of the lifted function at the image of $(x, y)$ in the separation quotient is the same as the limit behavior of the original function at $(x, y)$.
SeparationQuotient.tendsto_lift₂_nhdsWithin theorem
{f : X → Y → α} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d} {x : X} {y : Y} {s : Set (SeparationQuotient X × SeparationQuotient Y)} {l : Filter α} : Tendsto (uncurry <| lift₂ f hf) (𝓝[s] (mk x, mk y)) l ↔ Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l
Full source 
@[simp] theorem tendsto_lift₂_nhdsWithin {f : X → Y → α}
    {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d} {x : X} {y : Y}
    {s : Set (SeparationQuotientSeparationQuotient X × SeparationQuotient Y)} {l : Filter α} :
    TendstoTendsto (uncurry <| lift₂ f hf) (𝓝[s] (mk x, mk y)) l ↔
      Tendsto (uncurry f) (𝓝[Prod.map mk mk ⁻¹' s] (x, y)) l := by
  rw [nhdsWithin, ← map_prod_map_mk_nhds, ← Filter.push_pull, comap_principal]
  rfl
Limit Preservation Under Lifting to Separation Quotient Within a Subset
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y \to \alpha$ a binary function that respects the inseparable relation (i.e., $f(a, b) = f(c, d)$ whenever $a \sim_i c$ in $X$ and $b \sim_i d$ in $Y$), and $x \in X$, $y \in Y$ points. For any subset $s$ of $\text{SeparationQuotient}\, X \times \text{SeparationQuotient}\, Y$ and any filter $l$ on $\alpha$, the following are equivalent: 1. The lifted function $\text{lift}_2\, f\, hf$ tends to $l$ along the neighborhood filter of $(\text{mk}\, x, \text{mk}\, y)$ restricted to $s$. 2. The original function $f$ tends to $l$ along the neighborhood filter of $(x, y)$ restricted to the preimage of $s$ under the product map $\text{mk} \times \text{mk}$. In other words: \[ \lim_{\substack{(x',y') \to (\text{mk}\,x, \text{mk}\,y) \\ (x',y') \in s}} \text{lift}_2\, f\, hf\, (x', y') = l \quad \Leftrightarrow \quad \lim_{\substack{(x',y') \to (x,y) \\ (\text{mk}\,x', \text{mk}\,y') \in s}} f(x', y') = l \]
SeparationQuotient.continuousAt_lift₂ theorem
{f : X → Y → Z} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d} {x : X} {y : Y} : ContinuousAt (uncurry <| lift₂ f hf) (mk x, mk y) ↔ ContinuousAt (uncurry f) (x, y)
Full source 
@[simp]
theorem continuousAt_lift₂ {f : X → Y → Z} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d}
    {x : X} {y : Y} :
    ContinuousAtContinuousAt (uncurry <| lift₂ f hf) (mk x, mk y) ↔ ContinuousAt (uncurry f) (x, y) :=
  tendsto_lift₂_nhds
Continuity at Points is Preserved Under Lifting to Separation Quotient
Informal description
For any binary function $f \colon X \to Y \to Z$ that respects the inseparable relation (i.e., $f(a, b) = f(c, d)$ whenever $a$ and $c$ are inseparable in $X$ and $b$ and $d$ are inseparable in $Y$), and for any points $x \in X$ and $y \in Y$, the following are equivalent: 1. The lifted function $\operatorname{uncurry}(\operatorname{lift}_2\, f\, hf)$ is continuous at $(\operatorname{mk}(x), \operatorname{mk}(y))$ in the product space of separation quotients. 2. The original function $\operatorname{uncurry}\, f$ is continuous at $(x, y)$ in the product space $X \times Y$.
SeparationQuotient.continuousWithinAt_lift₂ theorem
{f : X → Y → Z} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d} {s : Set (SeparationQuotient X × SeparationQuotient Y)} {x : X} {y : Y} : ContinuousWithinAt (uncurry <| lift₂ f hf) s (mk x, mk y) ↔ ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (x, y)
Full source 
@[simp] theorem continuousWithinAt_lift₂ {f : X → Y → Z}
    {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d}
    {s : Set (SeparationQuotientSeparationQuotient X × SeparationQuotient Y)} {x : X} {y : Y} :
    ContinuousWithinAtContinuousWithinAt (uncurry <| lift₂ f hf) s (mk x, mk y) ↔
      ContinuousWithinAt (uncurry f) (Prod.map mk mk ⁻¹' s) (x, y) :=
  tendsto_lift₂_nhdsWithin
Continuity Within a Subset is Preserved Under Lifting to Separation Quotient
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y \to Z$ a binary function that respects the inseparable relation (i.e., $f(a, b) = f(c, d)$ whenever $a \sim_i c$ in $X$ and $b \sim_i d$ in $Y$), and $x \in X$, $y \in Y$ points. For any subset $s$ of $\text{SeparationQuotient}\, X \times \text{SeparationQuotient}\, Y$, the following are equivalent: 1. The lifted function $\text{uncurry}(\text{lift}_2\, f\, hf)$ is continuous at $(\text{mk}\, x, \text{mk}\, y)$ within $s$. 2. The original function $\text{uncurry}\, f$ is continuous at $(x, y)$ within the preimage of $s$ under the product map $\text{mk} \times \text{mk}$. In other words: \[ \text{uncurry}(\text{lift}_2\, f\, hf) \text{ is continuous at } (\text{mk}\, x, \text{mk}\, y) \text{ within } s \quad \Leftrightarrow \quad \text{uncurry}\, f \text{ is continuous at } (x, y) \text{ within } (\text{mk} \times \text{mk})^{-1}(s) \]
SeparationQuotient.continuousOn_lift₂ theorem
{f : X → Y → Z} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d} {s : Set (SeparationQuotient X × SeparationQuotient Y)} : ContinuousOn (uncurry <| lift₂ f hf) s ↔ ContinuousOn (uncurry f) (Prod.map mk mk ⁻¹' s)
Full source 
@[simp]
theorem continuousOn_lift₂ {f : X → Y → Z} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d}
    {s : Set (SeparationQuotientSeparationQuotient X × SeparationQuotient Y)} :
    ContinuousOnContinuousOn (uncurry <| lift₂ f hf) s ↔ ContinuousOn (uncurry f) (Prod.map mk mk ⁻¹' s) := by
  simp_rw [ContinuousOn, (surjective_mk.prodMap surjective_mk).forall, Prod.forall, Prod.map,
    continuousWithinAt_lift₂]
  rfl
Continuity of Lifted Binary Function on Separation Quotient ↔ Continuity on Preimage
Informal description
Let $X$ and $Y$ be topological spaces, $f : X \to Y \to Z$ a binary function that respects the inseparable relation (i.e., $f\, a\, b = f\, c\, d$ whenever $a \sim_i c$ and $b \sim_i d$), and $s$ a subset of $\text{SeparationQuotient}\, X \times \text{SeparationQuotient}\, Y$. Then the lifted function $\text{uncurry}(\text{lift₂}\, f\, hf)$ is continuous on $s$ if and only if $\text{uncurry}\, f$ is continuous on the preimage of $s$ under the product map $\text{mk} \times \text{mk}$.
SeparationQuotient.continuous_lift₂ theorem
{f : X → Y → Z} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d} : Continuous (uncurry <| lift₂ f hf) ↔ Continuous (uncurry f)
Full source 
@[simp]
theorem continuous_lift₂ {f : X → Y → Z} {hf : ∀ a b c d, (a ~ᵢ c) → (b ~ᵢ d) → f a b = f c d} :
    ContinuousContinuous (uncurry <| lift₂ f hf) ↔ Continuous (uncurry f) := by
  simp only [continuous_iff_continuousOn_univ, continuousOn_lift₂, preimage_univ]
Continuity of Lifted Binary Function on Separation Quotient ↔ Continuity of Original Function
Informal description
Let $X$ and $Y$ be topological spaces, and let $f : X \to Y \to Z$ be a binary function such that for any $a, b, c, d$, if $a$ and $c$ are inseparable in $X$ and $b$ and $d$ are inseparable in $Y$, then $f(a, b) = f(c, d)$. Then the lifted function $\text{uncurry}(\text{lift₂}\, f\, hf)$ is continuous if and only if $\text{uncurry}\, f$ is continuous.
continuous_congr_of_inseparable theorem
(h : ∀ x, f x ~ᵢ g x) : Continuous f ↔ Continuous g
Full source 
theorem continuous_congr_of_inseparable (h : ∀ x, f x ~ᵢ g x) :
    ContinuousContinuous f ↔ Continuous g := by
  simp_rw [SeparationQuotient.isInducing_mk.continuous_iff (Y := Y)]
  exact continuous_congr fun x ↦ SeparationQuotient.mk_eq_mk.mpr (h x)
Continuity is preserved under pointwise inseparability
Informal description
For two functions $f, g : X \to Y$ between topological spaces such that $f(x)$ and $g(x)$ are inseparable for all $x \in X$, the function $f$ is continuous if and only if $g$ is continuous.