map_inf_le — Mathlib

English

The image of an intersection is below the intersection of images: map f (L ⊓ M) ≤ map f L ⊓ map f M.

Русский

Образование пересечения подалгебр через f не превышает пересечение образований: map f (L ⊓ M) ≤ map f L ⊓ map f M.

LaTeX

$$$\operatorname{map} f (L \cap M) \le \operatorname{map} f L \cap \operatorname{map} f M$$$

Lean4

theorem map_inf_le (L M : BooleanSubalgebra α) (f : BoundedLatticeHom α β) : map f (L ⊓ M) ≤ map f L ⊓ map f M :=
  map_mono.map_inf_le _ _

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