sup_lt_iff — Mathlib

English

Let α be a linear order equipped with a lattice structure. For any b, c, a in α, we have sup(b, c) < a if and only if b < a and c < a.

Русский

Пусть α упорядочено линейно и имеет структуру решётки. Для любых b, c, a ∈ α выполняется: sup(b, c) < a тогда и только тогда, когда b < a и c < a.

LaTeX

$$$ b \vee c < a \iff b < a \land c < a $$$

Lean4

@[simp]
theorem sup_lt_iff : b ⊔ c < a ↔ b < a ∧ c < a :=
  ⟨fun h => ⟨le_sup_left.trans_lt h, le_sup_right.trans_lt h⟩, fun h => sup_ind (p := (· < a)) b c h.1 h.2⟩

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