map_iSup — Mathlib

English

For any index set i, the image of the supremum (iSup) of a family of intermediate fields under f is the supremum of the images:

Русский

Для произвольного множества индексов i образ объединения (iSup) семейства промежуточных полей под f равен объединению образов:

LaTeX

$$$\operatorname{map} f\, (\bigvee_i s_i) = \bigvee_i \operatorname{map} f\,(s_i)$$$

Lean4

theorem map_iSup {ι : Sort*} (f : E →ₐ[F] K) (s : ι → IntermediateField F E) : (iSup s).map f = ⨆ i, (s i).map f :=
  (gc_map_comap f).l_iSup

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