English
The topological space realized by the standard open-set realizer id coincides with the given topological structure on α.
Русский
Реализатор Realizer.id порождает ту же топологию, что и исходную на α.
LaTeX
$$$\\text{Realizer.id} = \\text{topology on open sets}$$$
Lean4
/-- The topological space realizer made of the open sets. -/
protected def id : Realizer α :=
⟨{ x : Set α // IsOpen x },
{ f := Subtype.val
top := fun _ ↦ ⟨univ, isOpen_univ⟩
top_mem := mem_univ
inter := fun ⟨_x, h₁⟩ ⟨_y, h₂⟩ _a _h₃ ↦ ⟨_, h₁.inter h₂⟩
inter_mem := fun ⟨_x, _h₁⟩ ⟨_y, _h₂⟩ _a ↦ id
inter_sub := fun ⟨_x, _h₁⟩ ⟨_y, _h₂⟩ _a _h₃ ↦ Subset.refl _ },
ext Subtype.property fun _x _s h ↦
let ⟨t, h, o, m⟩ := mem_nhds_iff.1 h
⟨⟨t, o⟩, m, h⟩⟩
