compl_eq_bot — Mathlib

English

If a prepartition π is a partition, then its complement is the bottom element (empty).

Русский

Если предразбиение π является разбиением, то его дополнение равно нижнему элементу (пустому предразбиению).

LaTeX

$$$ \\forall \\pi:\\mathrm{Prepartition}(I),\\ \\mathrm{IsPartition}(\\pi) \\;\\Rightarrow\\; \\pi.\\mathrm{compl} = \\bot$$$

Lean4

theorem compl_eq_bot {π : Prepartition I} (h : IsPartition π) : π.compl = ⊥ := by
  rw [← iUnion_eq_empty, iUnion_compl, h.iUnion_eq, diff_self]

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