comp_subset_self

Mathlib.Topology.UniformSpace.Ultra.Basic

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

English

If s is transitive, then the composition of s with itself is contained in s: s ∘ s ⊆ s.

Русский

Если s транзитивно, то композиция s с самой собой содержится в s: s ∘ s ⊆ s.

LaTeX

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

Lean4

theorem comp_subset_self {s : Set (X × X)} (h : IsTransitiveRel s) : s ○ s ⊆ s := fun ⟨_, _⟩ ⟨_, hxz, hzy⟩ ↦ h hxz hzy

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

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

Разделы

Аффилиация

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