comap_inf_map_of_injective — Mathlib

English

For any S, T ⊆ M, the comap of the infimum of their maps equals the infimum of S and T themselves: (S.map f ⊓ T.map f).comap f = S ⊓ T.

Русский

Комап инфимума образов S и T равен инфимуму S и T: (S.map f ⊓ T.map f).comap f = S ⊓ T.

LaTeX

$$(S.map f ⊓ T.map f).comap f = S ⊓ T$$

Lean4

@[to_additive]
theorem comap_inf_map_of_injective (S T : Subsemigroup M) : (S.map f ⊓ T.map f).comap f = S ⊓ T :=
  (gciMapComap hf).u_inf_l _ _

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