le_sup_iff — Mathlib

English

In a linear order, a ≤ b ⊔ c iff a ≤ b or a ≤ c.

Русский

В линейном порядке a ≤ b ∨ c эквивалентно a ≤ b или a ≤ c.

LaTeX

$$$a \le b \vee c \iff a \le b \\lor a \le c$$$

Lean4

@[simp]
theorem le_sup_iff : a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c := by
  exact
    ⟨fun h => (le_total c b).imp (fun bc => by rwa [sup_eq_left.2 bc] at h) (fun bc => by rwa [sup_eq_right.2 bc] at h),
      fun h => h.elim le_sup_of_le_left le_sup_of_le_right⟩

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