iso_map — Mathlib

English

The map iso_map C J is bijective (the underlying continuous map is a bijection).

Русский

Отображение iso_map C J является биекцией (соответствующее непрерывное отображение — биекция).

LaTeX

$$$$ \\operatorname{Bijective}(\\mathrm{iso\\_map}\\, C\\, J). $$$$

Lean4

/-- The objectwise map in the isomorphism `spanFunctor ≅ Profinite.indexFunctor`. -/
def iso_map : C(π C J, (IndexFunctor.obj C J)) :=
  ⟨fun x ↦
    ⟨fun i ↦ x.val i.val, by
      rcases x with ⟨x, y, hy, rfl⟩
      refine ⟨y, hy, ?_⟩
      ext ⟨i, hi⟩
      simp [precomp, Proj, hi]⟩,
    by
    refine Continuous.subtype_mk (continuous_pi fun i ↦ ?_) _
    exact (continuous_apply i.val).comp continuous_subtype_val⟩

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