map₂_inf_subset_right — Mathlib

English

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

Русский

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

LaTeX

$$$ map_2 m f (g_1 \sqcap g_2) \leq map_2 m f g_1 \sqcap map_2 m f g_2 $$$

Lean4

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

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