sup_eq_right — Mathlib

English

If a ≤ b, then the supremum a ⊔ b is equivalent to b under the CauSeq equivalence.

Русский

Если a ≤ b, то a ⊔ b эквивалентно b по отношению эквив., используемому в CauSeq.

LaTeX

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

Lean4

protected theorem sup_eq_right {a b : CauSeq α abs} (h : a ≤ b) : a ⊔ b ≈ b :=
  by
  obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h
  · intro _ _
    refine ⟨i, fun j hj => ?_⟩
    dsimp
    rw [← max_sub_sub_right]
    rwa [sub_self, max_eq_right, abs_zero]
    rw [sub_nonpos, ← sub_nonneg]
    exact ε0.le.trans (h _ hj)
  · refine Setoid.trans (sup_equiv_sup h (Setoid.refl _)) ?_
    rw [CauSeq.sup_idem]

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