comap_inf_map_of_injective — Mathlib

English

For any L-substructures S, T of M, the comap of the infimum of their mapped counterparts equals the infimum of the original: (S.map f ⊓ T.map f).comap f = S ⊓ T.

Русский

Для любых L-подструктур S, T M выполняется: comap f(S.map f ⊓ T.map f) = S ⊓ T.

LaTeX

$$$\forall S,T \in \mathrm{Sub}_L(M), (S.map f \sqcap T.map f).\mathrm{comap} f = S \sqcap T$$$

Lean4

theorem comap_inf_map_of_injective (S T : L.Substructure M) : (S.map f ⊓ T.map f).comap f = S ⊓ T :=
  (gciMapComap hf).u_inf_l _ _

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