sup_le — Mathlib

English

If a ≤ c and b ≤ c, then a ⊔ b ≤ c.

Русский

Если a ≤ c и b ≤ c, то a ⊔ b ≤ c.

LaTeX

$$$\forall a,b,c \in \mathrm{CauSeq}(\alpha, \mathrm{abs}),\; a \le c \land b \le c \Rightarrow a \vee b \le c$$$

Lean4

protected theorem sup_le {a b c : CauSeq α abs} (ha : a ≤ c) (hb : b ≤ c) : a ⊔ b ≤ c :=
  by
  obtain ha | ha := ha
  · obtain hb | hb := hb
    · exact Or.inl (CauSeq.sup_lt ha hb)
    · replace ha := le_of_le_of_eq ha.le (Setoid.symm hb)
      refine le_of_le_of_eq (Or.inr ?_) hb
      exact CauSeq.sup_eq_right ha
  · replace hb := le_of_le_of_eq hb (Setoid.symm ha)
    refine le_of_le_of_eq (Or.inr ?_) ha
    exact CauSeq.sup_eq_left hb

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