not_infIrred — Mathlib

English

Not InfIrred a is equivalent to IsMax a or there exist b,c with b ⊓ c = a and a is strictly less than both.

Русский

Not InfIrred a эквивалентно IsMax a или существует b,c такие что b ⊓ c = a и a строго меньше чем оба.

LaTeX

$$¬InfIrred\ a \iff IsMax\ a ∨ ∃ b c, b ⊓ c = a ∧ a < b ∧ a < c$$

Lean4

@[simp]
theorem not_infIrred : ¬InfIrred a ↔ IsMax a ∨ ∃ b c, b ⊓ c = a ∧ a < b ∧ a < c :=
  @not_supIrred αᵒᵈ _ _

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