English
If f is injective and continuous, then the target being T0 implies X is T0.
Русский
Если f инъективно и непрерывно, и цель — T0, то источник — T0.
LaTeX
$$$\text{If } hf: Injective(f) \text{ and } hf': Continuous(f) \text{ and } [T0Space Y], \text{ then } [T0Space X].$$$
Lean4
/-- Given an open finite set `S` in a T₀ space, there is some `x ∈ S` such that `{x}` is open. -/
theorem exists_isOpen_singleton_of_isOpen_finite [T0Space X] {s : Set X} (hfin : s.Finite) (hne : s.Nonempty)
(ho : IsOpen s) : ∃ x ∈ s, IsOpen ({ x } : Set X) :=
by
lift s to Finset X using hfin
induction s using Finset.strongInductionOn
rename_i s ihs
rcases em (∃ t, t ⊂ s ∧ t.Nonempty ∧ IsOpen (t : Set X)) with (⟨t, hts, htne, hto⟩ | ht)
· rcases ihs t hts htne hto with ⟨x, hxt, hxo⟩
exact ⟨x, hts.1 hxt, hxo⟩
· -- Porting note: was `rcases minimal_nonempty_open_eq_singleton ho hne _ with ⟨x, hx⟩`
-- https://github.com/leanprover-community/batteries/issues/116
rsuffices ⟨x, hx⟩ : ∃ x, s.toSet = { x }
· exact ⟨x, hx.symm ▸ rfl, hx ▸ ho⟩
refine minimal_nonempty_open_eq_singleton ho hne ?_
refine fun t hts htne hto => of_not_not fun hts' => ht ?_
lift t to Finset X using s.finite_toSet.subset hts
exact ⟨t, ssubset_iff_subset_ne.2 ⟨hts, mt Finset.coe_inj.2 hts'⟩, htne, hto⟩
