map_iSup_comap_of_surjective — Mathlib

English

Same as 148532 with alternative phrasing: map f (iSup_i (S_i.comap f)) = iSup_i S_i.

Русский

То же, что и 148532, выраженное иначе: map f (iSup_i (S_i.comap f)) = iSup_i S_i.

LaTeX

$$$\forall (S_i) : ι \to \mathrm{Sub}_L(N), \mathrm{map}_f(\bigvee_i \mathrm{comap}_f(S_i)) = \bigvee_i S_i$$$

Lean4

theorem map_iSup_comap_of_surjective (S : ι → L.Substructure N) : (⨆ i, (S i).comap f).map f = ⨆ i, S i :=
  (giMapComap hf).l_iSup_u _

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