range_liftAux — Mathlib

English

The range of liftAux(I', hI') equals the real-subalgebra adjoinℝ{I'}.

Русский

Образ функции liftAux(I', hI') равен реальной подпалгебре, порожденной I'.

LaTeX

$$$ \operatorname{range}(\mathrm{liftAux}(I',hI')) = \operatorname{adjoin}_{\\mathbb{R}}(\{ I' \}). $$$

Lean4

@[simp]
theorem range_liftAux (I' : A) (hI') : (liftAux I' hI').range = Algebra.adjoin ℝ { I' } := by
  simp_rw [← Algebra.map_top, ← adjoin_I, AlgHom.map_adjoin, Set.image_singleton, liftAux_apply_I]

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