comap

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Equivalence.comap

English

If r is an equivalence, then r on f is an equivalence.

Русский

Если r является эквивалентностью, то r on f — эквивалентность.

LaTeX

$$$\forall r:\beta\to\beta\to \mathrm{Prop},\; \mathrm{Equivalence}(r) \Rightarrow \mathrm{Equivalence}(r\ on\ f)$$$

Lean4

theorem comap (h : Equivalence r) (f : α → β) : Equivalence (r on f) :=
  ⟨fun a ↦ h.refl (f a), h.symm, h.trans⟩

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

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

Разделы

Аффилиация

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