comap_inf — Mathlib

English

Let s, t be subfields of L and f: K →+* L. The preimage of the meet equals the meet of preimages: (s ⊓ t).comap f = s.comap f ⊓ t.comap f.

Русский

Пусть s, t — подполе L и f : K →+* L. Предобраз пересечения равен пересечению предобразов: (s ⊓ t).comap f = s.comap f ⊓ t.comap f.

LaTeX

$$$$(s \sqcap t).comap f = s.comap f \sqcap t.comap f$$$$

Lean4

theorem comap_inf (s t : Subfield L) (f : K →+* L) : (s ⊓ t).comap f = s.comap f ⊓ t.comap f :=
  (gc_map_comap f).u_inf

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