isTransitiveRel_iff_comp_subset_self

English

A relation s is transitive if and only if its square is contained in itself: IsTransitive(s) ⇔ s ∘ s ⊆ s.

Русский

Отношение s транзитивно тогда и только тогда, когда его квадрат содержится в самом s: Transitive(s) ⇔ s ∘ s ⊆ s.

LaTeX

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

Lean4

theorem isTransitiveRel_iff_comp_subset_self {s : Set (X × X)} : IsTransitiveRel s ↔ s ○ s ⊆ s :=
  ⟨IsTransitiveRel.comp_subset_self, fun h _ _ _ hx hy ↦ h ⟨_, hx, hy⟩⟩

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