comap

Mathlib.Logic.Relation

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

English

If r is transitive, then r on f is transitive.

Русский

Если r транзитивно, то r on f транзитивно.

LaTeX

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

Lean4

theorem comap (h : Transitive r) (f : α → β) : Transitive (r on f) := fun _ _ _ hab hbc ↦ h hab hbc

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

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

Разделы

Аффилиация

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