inf_eq_right — Mathlib

English

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

Русский

Если b ≤ a, то a ⊓ b эквивалентно b.

LaTeX

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

Lean4

protected theorem inf_eq_right {a b : CauSeq α abs} (h : b ≤ a) : a ⊓ b ≈ b :=
  by
  obtain ⟨ε, ε0 : _ < _, i, h⟩ | h := h
  · intro _ _
    refine ⟨i, fun j hj => ?_⟩
    dsimp
    rw [← min_sub_sub_right]
    rwa [sub_self, min_eq_right, abs_zero]
    exact ε0.le.trans (h _ hj)
  · refine Setoid.trans (inf_equiv_inf (Setoid.symm h) (Setoid.refl _)) ?_
    rw [CauSeq.inf_idem]

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