coe_ofBijective — Mathlib

English

If f is a bijective coalgebra morphism, then CoalgEquiv.ofBijective hf yields a coalgebra equivalence whose forward map is f.

Русский

Если f — биективный коалгоморфизм, то CoalgEquiv.ofBijective hf задаёт коалгебраическую эквивалентность, прямой картой которой является f.

LaTeX

$$$\\mathrm{coe\\_ofBijective} : (hf : \\mathrm{Function.Bijective} (\\mathrm{CoalgHom}.\\mathrm{funLike}.\\mathrm{coe} f)) \\Rightarrow (\\mathrm{CoalgEquiv}.ofBijective hf : A \\to B) = f$$$

Lean4

@[simp]
theorem coe_ofBijective : (CoalgEquiv.ofBijective hf : A → B) = f :=
  rfl

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