sub_eq_top_iff — Mathlib

English

In WithTop α, the equation a − b = ⊤ holds exactly when a = ⊤ and b ≠ ⊤.

Русский

В WithTop α равенство a − b = ⊤ держится точно тогда, когда a = ⊤ и b ≠ ⊤.

LaTeX

$$$\forall a,b \in WithTop \alpha\,(a - b = \top) \iff (a = \top \land b \neq \top)$$$

Lean4

@[simp]
theorem sub_eq_top_iff {a b : WithTop α} : a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤ := by
  induction a <;> induction b <;>
    simp only [← coe_sub, coe_ne_top, sub_top, top_sub_coe, false_and, Ne, not_true_eq_false, not_false_eq_true,
      and_false, and_self]

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