ext — Mathlib

English

Two realizers define the same topology iff they agree on nhds for all sets.

Русский

Два реализатора задают одну и ту же топологию, если они согласованы по nhds для всех множеств.

LaTeX

$$[Extensionality for Realizers: F.toTopsp = T given pointwise nhds correspondence]$$

Lean4

theorem ext [T : TopologicalSpace α] {σ : Type*} {F : Ctop α σ} (H₁ : ∀ a, IsOpen (F a))
    (H₂ : ∀ a s, s ∈ 𝓝 a → ∃ b, a ∈ F b ∧ F b ⊆ s) : F.toTopsp = T :=
  ext' fun a s ↦ ⟨H₂ a s, fun ⟨_b, h₁, h₂⟩ ↦ mem_nhds_iff.2 ⟨_, h₂, H₁ _, h₁⟩⟩

Похожие утверждения