parts_eq_empty_iff — Mathlib

English

The parts of P are empty if and only if a equals ⊥.

Русский

Блоки разбиения P пусты тогда и только тогда, когда a = ⊥.

LaTeX

$$$P.\text{parts} = \emptyset \iff a = \bot$$$

Lean4

@[simp]
theorem parts_eq_empty_iff : P.parts = ∅ ↔ a = ⊥ :=
  by
  simp_rw [← P.sup_parts]
  refine ⟨fun h ↦ ?_, fun h ↦ eq_empty_iff_forall_notMem.2 fun b hb ↦ P.bot_notMem ?_⟩
  · rw [h]
    exact Finset.sup_empty
  · rwa [← le_bot_iff.1 ((le_sup hb).trans h.le)]

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