not_supIrred — Mathlib

English

Not SupIrred a holds exactly when either a is minimal or a can be written as a join b ⊔ c with b < a and c < a.

Русский

Не SupIrred a эквивалентно тому, что a минимален или существует разложение a = b ⊔ c с b < a и c < a.

LaTeX

$$¬SupIrred\ a \iff IsMin\ a \lor \exists b\ c, b ⊔ c = a ∧ b < a ∧ c < a$$

Lean4

@[simp]
theorem not_supIrred : ¬SupIrred a ↔ IsMin a ∨ ∃ b c, b ⊔ c = a ∧ b < a ∧ c < a :=
  by
  rw [SupIrred, not_and_or]
  push_neg
  rw [exists₂_congr]
  simp +contextual [@eq_comm _ _ a]

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