comp_eq_of_idRel_subset

Mathlib.Topology.UniformSpace.Ultra.Basic

URI: https://scilib.ai/kg/mathlib#IsTransitiveRel.comp_eq_of_idRel_subset

← MathLib Explorer

English

If s is transitive and idRel ⊆ s, then s ∘ s = s.

Русский

Если s транзитивно и idRel ⊆ s, то s ∘ s = s.

LaTeX

$$$\text{Transitive}(s) \land \text{idRel} \subseteq s \Rightarrow s \circ s = s$$$

Lean4

theorem comp_eq_of_idRel_subset {s : Set (X × X)} (h : IsTransitiveRel s) (h' : idRel ⊆ s) : s ○ s = s :=
  le_antisymm h.comp_subset_self (subset_comp_self h')

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

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

Разделы

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

Аффилиация

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