eq_iff_le_not_lt — Mathlib

English

Under decidable order, a = b iff a ≤ b and not a < b.

Русский

При решаемом порядке a = b эквивалентно a ≤ b и не a < b.

LaTeX

$$$ a = b \iff a \le b \land \lnot (a < b) $$$

Lean4

protected theorem eq_iff_le_not_lt [DecidableLE α] : a = b ↔ a ≤ b ∧ ¬a < b :=
  ⟨fun h ↦ ⟨h.le, h ▸ lt_irrefl _⟩, fun ⟨h₁, h₂⟩ ↦
    h₁.antisymm <| Decidable.byContradiction fun h₃ ↦ h₂ (h₁.lt_of_not_ge h₃)⟩

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