toHom_range

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Equiv.toHom_range

← MathLib Explorer

English

An equivalence f:M ≃[L] N has the property that f.toHom is surjective onto N.

Русский

Эквивалентность f:M ≃[L] N обладает свойством сюръективности на N через f.toHom.

LaTeX

$$$f.toHom.range = \\top$$$

Lean4

theorem toHom_range (f : M ≃[L] N) : f.toHom.range = ⊤ :=
  by
  ext n
  simp only [Hom.mem_range, coe_toHom, Substructure.mem_top, iff_true]
  exact ⟨f.symm n, apply_symm_apply _ _⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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