nhdsKer_subset_iff — Mathlib

English

nhdsKer s ⊆ t iff ∃ U open with s ⊆ U ⊆ t.

Русский

nhdsKer s ⊆ t эквивалентно существованию открытого U с s ⊆ U ⊆ t.

LaTeX

$$nhdsKer s ⊆ t ⇔ ∃ U, IsOpen U ∧ s ⊆ U ∧ U ⊆ t$$

Lean4

theorem nhdsKer_subset_iff : nhdsKer s ⊆ t ↔ ∃ U, IsOpen U ∧ s ⊆ U ∧ U ⊆ t :=
  ⟨fun h ↦ ⟨nhdsKer s, isOpen_nhdsKer, subset_nhdsKer, h⟩, fun ⟨_U, hU, hsU, hUt⟩ ↦ (nhdsKer_minimal hsU hU).trans hUt⟩

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