le_iff_eq — Mathlib

English

Let α be a partially ordered set with a bottom element. If a is an atom and b ≠ ⊥, then b ≤ a if and only if b = a.

Русский

Пусть α — частично упорядоченное множество с нулём. Если a — атом, а b ≠ ⊥, то b ≤ a тогда и только тогда, когда b = a.

LaTeX

$$IsAtom a → b ≠ ⊥ → (b ≤ a) \Leftrightarrow (b = a)$$

Lean4

theorem le_iff_eq (ha : IsAtom a) (hb : b ≠ ⊥) : b ≤ a ↔ b = a :=
  ha.le_iff.trans <| or_iff_right hb

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