iInter_le_mem — Mathlib

English

For a finite index set, the intersection up to n lies in C if all s(i) ∈ C.

Русский

Для конечного множества индексов пересечение до n лежит в C, если все s(i) ∈ C.

LaTeX

$$$\text{If } s(n)\in C \ \forall n, \text{ then } \bigcap_{i≤n} s(i)\in C.$$$

Lean4

theorem iInter_le_mem (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ n, s n ∈ C) (n : ℕ) : (⋂ i ≤ n, s i) ∈ C := by
  induction n with
  | zero => simp [hs 0]
  | succ n hn => rw [biInter_le_succ]; exact hC.inter_mem hn (hs _)

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