add_eq_top_iff — Mathlib

English

For any a,b in PartENat, a + b = ⊤ if and only if a = ⊤ or b = ⊤.

Русский

Для любых a,b из PartENat, a + b = ⊤ тогда и только тогда, когда a = ⊤ или b = ⊤.

LaTeX

$$$ \forall a,b : \mathrm{PartENat}, a + b = \top \iff a = \top \lor b = \top $$$

Lean4

theorem add_eq_top_iff {a b : PartENat} : a + b = ⊤ ↔ a = ⊤ ∨ b = ⊤ :=
  by
  refine PartENat.casesOn a ?_ ?_ <;> refine PartENat.casesOn b ?_ ?_ <;> simp [top_add, add_top]
  simp only [← Nat.cast_add, PartENat.natCast_ne_top, forall_const, not_false_eq_true]

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