English
Let X be a topological space. The separation quotient SeperationQuotient(X) is T1 if and only if X is R0.
Русский
Пусть X — топологическое пространство. Фактор-пространство SeparationQuotient(X) является T1 тогда и только если X обладает свойством R0.
LaTeX
$$$ T1Space(\\mathrm{SeparationQuotient}(X)) \\iff R0Space(X). $$$
Lean4
theorem t1Space_iff : T1Space (SeparationQuotient X) ↔ R0Space X :=
by
rw [r0Space_iff, ((t1Space_TFAE (SeparationQuotient X)).out 0 9 :)]
constructor
· intro h x y xspecy
rw [← IsInducing.specializes_iff isInducing_mk, h xspecy] at *
· -- TODO is there are better way to do this,
-- so the case split produces `SeparationQuotient.mk` directly, rather than `Quot.mk`?
-- Currently we need the `change` statement to recover this.
rintro h ⟨x⟩ ⟨y⟩ sxspecsy
change mk _ = mk _
have xspecy : x ⤳ y := isInducing_mk.specializes_iff.mp sxspecsy
have yspecx : y ⤳ x := h xspecy
rw [mk_eq_mk, inseparable_iff_specializes_and]
exact ⟨xspecy, yspecx⟩
