map₂_inf_subset_left — Mathlib

English

The map₂ operation is monotone with respect to the left infimum: map₂ m (f₁ ⊓ f₂) g ≤ map₂ m f₁ g ⊓ map₂ m f₂ g.

Русский

map₂ монтонное относительно левой пересечения: map₂ m (f₁ ⊓ f₂) g ≤ map₂ m f₁ g ⊓ map₂ m f₂ g.

LaTeX

$$$ map_2 m (f_1 \sqcap f_2) g \leq map_2 m f_1 g \sqcap map_2 m f_2 g $$$

Lean4

theorem map₂_inf_subset_left : map₂ m (f₁ ⊓ f₂) g ≤ map₂ m f₁ g ⊓ map₂ m f₂ g :=
  Monotone.map_inf_le (fun _ _ ↦ map₂_mono_right) f₁ f₂

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