sup_equiv_sup — Mathlib

English

If a1 ≈ a2 and b1 ≈ b2 then a1 ⊔ b1 ≈ a2 ⊔ b2.

Русский

Если a1 ≈ a2 и b1 ≈ b2, то a1 ⊔ b1 ≈ a2 ⊔ b2.

LaTeX

$$$a_1 \approx a_2 \land b_1 \approx b_2 \Rightarrow a_1 \lor b_1 \approx a_2 \lor b_2.$$$

Lean4

theorem sup_equiv_sup {a₁ b₁ a₂ b₂ : CauSeq α abs} (ha : a₁ ≈ a₂) (hb : b₁ ≈ b₂) : a₁ ⊔ b₁ ≈ a₂ ⊔ b₂ :=
  by
  intro ε ε0
  obtain ⟨ai, hai⟩ := ha ε ε0
  obtain ⟨bi, hbi⟩ := hb ε ε0
  exact
    ⟨ai ⊔ bi, fun i hi =>
      (abs_max_sub_max_le_max (a₁ i) (b₁ i) (a₂ i) (b₂ i)).trans_lt
        (max_lt (hai i (sup_le_iff.mp hi).1) (hbi i (sup_le_iff.mp hi).2))⟩

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