sInter — Mathlib

English

If a set ℛ of relations on α contains only transitive relations, then their intersection ⋂ℛ is transitive.

Русский

Если множество ℛ отношений на α состоит только из транзитивных отношений, то их пересечение ⋂ℛ транзитивно.

LaTeX

$$$\forall \mathcal{R} \subseteq \{\text{SetRel } \alpha \alpha\},\ (\forall R \in \mathcal{R}, R.IsTrans) \Rightarrow (\bigcap \mathcal{R}).IsTrans$$

Lean4

protected theorem sInter {ℛ : Set <| SetRel α α} (hℛ : ∀ R ∈ ℛ, R.IsTrans) : SetRel.IsTrans (⋂₀ ℛ) where
  trans _a _b _c hab hbc R hR := (hℛ R hR).trans _ _ _ (hab R hR) <| hbc R hR

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