join_of_equivalence

Mathlib.Logic.Relation

URI: https://scilib.ai/kg/mathlib#Relation.join_of_equivalence

← MathLib Explorer

English

If r' is contained in an equivalence r, then from Join r' a b we deduce r a b.

Русский

Если r' ⊆ r и r является эквивалентностью, то Join r' a b ⇒ r a b.

LaTeX

$$$\\\\operatorname{Join} r' a b \\\\Rightarrow r a b$$$

Lean4

theorem join_of_equivalence {r' : α → α → Prop} (hr : Equivalence r) (h : ∀ a b, r' a b → r a b) : Join r' a b → r a b
  | ⟨_, hac, hbc⟩ => hr.trans (h _ _ hac) (hr.symm <| h _ _ hbc)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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