comp_of_injective

Mathlib.Logic.Pairwise

URI: https://scilib.ai/kg/mathlib#Pairwise.comp_of_injective

English

If r is pairwise and f is injective, then r on f is pairwise.

Русский

Если r держится попарно и f инъективна, то r на f держится попарно.

LaTeX

$$$\\operatorname{Pairwise}(r) \\land \\operatorname{Injective}(f) \\Rightarrow \\operatorname{Pairwise}(r\\ on\\ f)$$$

Lean4

theorem comp_of_injective (hr : Pairwise r) {f : β → α} (hf : Injective f) : Pairwise (r on f) := fun _ _ h ↦
  hr <| hf.ne h

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

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

Разделы

Аффилиация

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