le_antisymm_iff — Mathlib

English

Equality holds iff each is ≤ the other: a = b iff a ≤ b and b ≤ a.

Русский

Равенство выполняется тогда и только тогда, когда каждое не больше другого: a = b, если и только если a ≤ b и b ≤ a.

LaTeX

$$$a = b \leftrightarrow a \le b ∧ b \le a$$$

Lean4

theorem le_antisymm_iff : a = b ↔ a ≤ b ∧ b ≤ a :=
  ⟨fun e => ⟨le_of_eq e, le_of_eq e.symm⟩, fun ⟨h1, h2⟩ => le_antisymm h1 h2⟩

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