English
For any type α and element a' ∈ α, there exists a unique a ∈ α with a' = a.
Русский
Для любого типа α и элемента a' ∈ α существует единственный элемент a ∈ α такой, что a' = a.
LaTeX
$$$\exists! a:\alpha\; (a' = a)$$$
Lean4
/-- (Implementation) An auxiliary lemma for the proof that `TopCat` is finitary extensive. -/
noncomputable def finitaryExtensiveTopCatAux (Z : TopCat.{u}) (f : Z ⟶ TopCat.of (PUnit.{u + 1} ⊕ PUnit.{u + 1})) :
IsColimit
(BinaryCofan.mk (TopCat.pullbackFst f (TopCat.binaryCofan (TopCat.of PUnit) (TopCat.of PUnit)).inl)
(TopCat.pullbackFst f (TopCat.binaryCofan (TopCat.of PUnit) (TopCat.of PUnit)).inr)) :=
by
have h₁ :
Set.range (TopCat.pullbackFst f (TopCat.binaryCofan (.of PUnit) (.of PUnit)).inl) = f ⁻¹' Set.range Sum.inl :=
by
apply le_antisymm
· rintro _ ⟨x, rfl⟩; exact ⟨PUnit.unit, x.2.symm⟩
· rintro x ⟨⟨⟩, hx⟩; refine ⟨⟨⟨x, PUnit.unit⟩, hx.symm⟩, rfl⟩
have h₂ :
Set.range (TopCat.pullbackFst f (TopCat.binaryCofan (.of PUnit) (.of PUnit)).inr) = f ⁻¹' Set.range Sum.inr :=
by
apply le_antisymm
· rintro _ ⟨x, rfl⟩; exact ⟨PUnit.unit, x.2.symm⟩
· rintro x ⟨⟨⟩, hx⟩; refine ⟨⟨⟨x, PUnit.unit⟩, hx.symm⟩, rfl⟩
refine ((TopCat.binaryCofan_isColimit_iff _).mpr ⟨?_, ?_, ?_⟩).some
· refine ⟨(Homeomorph.prodPUnit Z).isEmbedding.comp .subtypeVal, ?_⟩
convert f.hom.2.1 _ isOpen_range_inl
· refine ⟨(Homeomorph.prodPUnit Z).isEmbedding.comp .subtypeVal, ?_⟩
convert f.hom.2.1 _ isOpen_range_inr
· convert Set.isCompl_range_inl_range_inr.preimage f
