disjoint_base_iUnion_openCell — Mathlib

English

The base D is disjoint from the union of all open cells: Disjoint D (⋃ (n) (j : cell C n), openCell n j).

Русский

База D дизъюнктна с объединением всех открытых клеток: Disjoint D ⋃_{n,j} openCell n j.

LaTeX

$$Disjoint\ D\ (\bigcup_{n} \bigcup_{j \in cell C n} openCell n j)$$

Lean4

theorem disjoint_base_iUnion_openCell [RelCWComplex C D] : Disjoint D (⋃ (n : ℕ) (j : cell C n), openCell n j) :=
  by
  simp_rw [disjoint_iff_inter_eq_empty, inter_iUnion, iUnion_eq_empty]
  intro n i
  rw [inter_comm, (disjointBase n i).inter_eq]

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