inter — Mathlib

English

If s and t are transitive relations, then their intersection s ∩ t is transitive.

Русский

Если s и t — транзитивные отношения, то их пересечение s ∩ t также транзитивно.

LaTeX

$$$\text{Transitive}(s) \land \text{Transitive}(t) \Rightarrow \text{Transitive}(s \cap t)$$$

Lean4

theorem inter {s t : Set (X × X)} (hs : IsTransitiveRel s) (ht : IsTransitiveRel t) : IsTransitiveRel (s ∩ t) :=
  fun _ _ _ h h' ↦ ⟨hs h.left h'.left, ht h.right h'.right⟩

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