iInter — Mathlib

English

The iInter of a family of symmetric relations is symmetric.

Русский

Произвольная бесконечная пересекающаяся операция над симметричными отношениями сохраняет симметричность.

LaTeX

$$IsSymmetricRel (Set.iInter fun i => U i)$$

Lean4

theorem iInter {U : (i : ι) → Set (α × α)} (hU : ∀ i, IsSymmetricRel (U i)) : IsSymmetricRel (⋂ i, U i) := by
  simp_rw [IsSymmetricRel, preimage_iInter, (hU _).eq]

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