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