sInter — Mathlib

English

If a family of SetRel relations is all symmetric, their intersection over all indices is symmetric.

Русский

Если семейство отношений симметрично, их пересечение по всем индексам симметрично.

LaTeX

$$For a family ℛ of relations, if ∀ R ∈ ℛ, R IsSymm, then IsSymm (⋂₀ ℛ)$$

Lean4

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

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