inf_mul₀ — Mathlib

English

Symmetry statement for left multiplication order isomorphisms.

Русский

Симметричное утверждение для левого умножения и изоморфизмов порядка.

LaTeX

$$OrderIso.mulLeft₀_symm( a, ha )$$

Lean4

theorem inf_mul₀ [SemilatticeInf G₀] [MulPosReflectLT G₀] {c : G₀} (hc : 0 ≤ c) (a b : G₀) :
    (a ⊓ b) * c = a * c ⊓ b * c := by
  obtain (rfl | hc) := hc.eq_or_lt
  · simp
  · exact (OrderIso.mulRight₀ c hc).map_inf a b

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