isPiSystem — Mathlib

English

If C is a semiring of sets, then C is a pi-system: for any s,t ∈ C, s ∩ t ∈ C.

Русский

Если C — полусистема множеств (полупрямой набор множеств), то C является пи‑системой: для любых s,t ∈ C выполняется s ∩ t ∈ C.

LaTeX

$$$\forall \alpha,\; \forall C \subseteq \mathcal{P}(\alpha),\; \text{IsSetSemiring}(C) \Rightarrow \forall s,t\in C,\ s\cap t\in C.$$$

Lean4

theorem isPiSystem (hC : IsSetSemiring C) : IsPiSystem C := fun s hs t ht _ ↦ hC.inter_mem s hs t ht

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