eq_of_forall_subset_iff — Mathlib

English

Let B be a topological basis for α. If s and t are open subsets of α and for every basis element U ∈ B we have U ⊆ s iff U ⊆ t, then s = t.

Русский

Пусть B является топологическим базисом для пространства α. Если s и t — открытые подмножества α и для каждого элемента базы U ∈ B выполнено U ⊆ s тогда и только если U ⊆ t, то s = t.

LaTeX

$$$\\text{If } B \\text{ is a topological basis and } s,t \\subseteq \\alpha\\text{ are open, and } \\forall U \\in B,\\ U \\subseteq s \\iff U \\subseteq t,\\text{ then } s = t.$$$

Lean4

theorem eq_of_forall_subset_iff {t : Set α} (hB : IsTopologicalBasis B) (hs : IsOpen s) (ht : IsOpen t)
    (h : ∀ U ∈ B, U ⊆ s ↔ U ⊆ t) : s = t :=
  by
  rw [hB.open_eq_sUnion' hs, hB.open_eq_sUnion' ht]
  exact congr_arg _ (Set.ext fun U ↦ and_congr_right <| h _)

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