range_lift — Mathlib

English

The range of the lift map equals the supremum of the component ranges.

Русский

Образ лифта равен наибольшему объединению образов компонент.

LaTeX

$$$(\mathrm{lift}_{L,\iota,G,f,gHg}).\mathrm{toHom}.\mathrm{range} = \bigvee_i (g i).\mathrm{toHom}.\mathrm{range}.$$$

Lean4

theorem range_lift : (lift L ι G f g Hg).toHom.range = ⨆ i, (g i).toHom.range :=
  by
  simp_rw [Hom.range_eq_map]
  rw [← iSup_range_of_eq_top, Substructure.map_iSup]
  simp_rw [Hom.range_eq_map, Substructure.map_map]
  rfl

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