inf_equiv_inf — 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 \land b_1 \approx a_2 \land b_2.$$$

Lean4

theorem inf_equiv_inf {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_min_sub_min_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))⟩

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