range_eq_iSup — Mathlib

English

The range of lift f equals the supremum of the component ranges: (lift f).range = ⨆ i, (f i).range.

Русский

Образ lift f равен верхней грани (верхней границы) компонент: (lift f).range = ⨆ i, (f i).range.

LaTeX

$$$ (\\mathrm{lift} f).\\mathrm{range} = \\bigsqcup_i (f_i).\\mathrm{range}$$$

Lean4

theorem range_eq_iSup {N} [Group N] (f : ∀ i, G i →* N) : (lift f).range = ⨆ i, (f i).range :=
  by
  apply le_antisymm (lift_range_le _ f fun i => le_iSup (fun i => MonoidHom.range (f i)) i)
  apply iSup_le _
  rintro i _ ⟨x, rfl⟩
  exact ⟨of x, by simp only [lift_of]⟩

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