sInter — Mathlib

English

If every member of a family of relations is transitive, their intersection is transitive.

Русский

Если каждый элемент семейства отношений транзитивен, их общая пересечение транзитивна.

LaTeX

$$$\forall s:\, s \text{ is a family of relations},\; (\forall i, i \in s) \Rightarrow \text{Transitive}(i) \Rightarrow \text{Transitive}\left(\bigcap s\right)$$$

Lean4

theorem sInter {s : Set (Set (X × X))} (h : ∀ i ∈ s, IsTransitiveRel i) : IsTransitiveRel (⋂₀ s) :=
  by
  rw [sInter_eq_iInter]
  exact IsTransitiveRel.iInter (by simpa)

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