equivRange

Mathlib.ModelTheory.Substructures

URI: https://scilib.ai/kg/mathlib#FirstOrder.Language.Embedding.equivRange

Lean4

/-- The equivalence between the domain and the range of an embedding `f`. -/
@[simps toEquiv_apply]
noncomputable def equivRange (f : M ↪[L] N) : M ≃[L] f.toHom.range
    where
  toFun := codRestrict f.toHom.range f f.toHom.mem_range_self
  invFun n := Classical.choose n.2
  left_inv m := f.injective (Classical.choose_spec (codRestrict f.toHom.range f f.toHom.mem_range_self m).2)
  right_inv := fun ⟨_, hn⟩ => Subtype.mk_eq_mk.2 (Classical.choose_spec hn)
  map_fun' {n} f x := by simp
  map_rel' {n} R x := by simp

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

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

Разделы

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

Аффилиация

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