iUnion_inter — Mathlib

English

Let X be a topological space and let u_i (i in I) be an open cover of X. Then for every subset s of X, the union over i of s ∩ u_i equals s.

Русский

Пусть X — топологическое пространство, {u_i} — открытое покрытие X. Тогда для каждого множества s ⊆ X выполняется ⋃_i (s ∩ u_i) = s.

LaTeX

$$$\mathrm{IsOpenCover}(u) \rightarrow \forall s \subseteq X, \bigcup_i (s \cap u_i) = s$$$

Lean4

theorem iUnion_inter (hu : IsOpenCover u) (s : Set X) : ⋃ i, s ∩ u i = s := by
  simp [← inter_iUnion, hu.iSup_set_eq_univ]

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