eval_surjective

Mathlib.RingTheory.AdicCompletion.Basic

URI: https://scilib.ai/kg/mathlib#AdicCompletion.eval_surjective

English

The image of eval I M n is the whole ambient target space, i.e., its range is ⊤.

Русский

Образ eval I M n равен всему пространству: образ равен ⊤.

LaTeX

$$$ \\mathrm{range}(\\mathrm{eval}\\, I\\, M\\, n) = \\top $$$

Lean4

theorem eval_surjective (n : ℕ) : Function.Surjective (eval I M n) := fun x ↦
  Quotient.inductionOn' x fun x ↦ ⟨of I M x, rfl⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru