map_inf — Mathlib

English

Mapping distributes over inf: the map of the infimum equals the infimum of the maps.

Русский

Отображение распределяет по Inf: отображение м1 ∧ м2 равно отображению m1 через f ∧ отображению m2 через f.

LaTeX

$$$$ (m_{1} \sqcap m_{2}).\mathrm{map}\, f = m_{1}.\mathrm{map}\, f \;\sqcap\; m_{2}.\mathrm{map}\, f $$$$

Lean4

@[simp]
theorem map_inf : (m₁ ⊓ m₂).map f = m₁.map f ⊓ m₂.map f :=
  (gc_comap_map f).u_inf

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