iInter — Mathlib

English

If each U_i is transitive, then the intersection over i of U_i is transitive.

Русский

Если каждый U_i транзитивен, то пересечение по i от U_i транзитивно.

LaTeX

$$$\forall i, \text{Transitive}(U(i)) \Rightarrow \text{Transitive}\left(\bigcap_i U(i)\right)$$$

Lean4

theorem iInter {ι : Type*} {U : (i : ι) → Set (X × X)} (hU : ∀ i, IsTransitiveRel (U i)) : IsTransitiveRel (⋂ i, U i) :=
  by
  intro _ _ _ h h'
  simp only [mem_iInter] at h h' ⊢
  intro i
  exact hU i (h i) (h' i)

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