isTrans_iInter — Mathlib

English

If R_i is transitive for all i in ι, then the indexed intersection ⋂i R_i is transitive.

Русский

Если для каждого i из ι отношение R_i транзитивно, то пересечение по индексу ⋂i R_i транзитивно.

LaTeX

$$$\forall (R : ι \to \text{SetRel } α α)\, [\forall i, (R i).IsTrans] \Rightarrow \ text{SetRel.IsTrans}(\bigcap_{i} R i)$$

Lean4

instance isTrans_iInter {R : ι → SetRel α α} [∀ i, (R i).IsTrans] : SetRel.IsTrans (⋂ i, R i) :=
  .sInter <| by simpa

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