finite_memPartition — Mathlib

English

For every n, memPartition(f,n) is a finite family of sets.

Русский

Для каждого n множество memPartition(f,n) является конечной системой подмножеств.

LaTeX

$$$\\operatorname{Finite}(\\operatorname{memPartition}(f,n))$$$

Lean4

theorem finite_memPartition (f : ℕ → Set α) (n : ℕ) : Set.Finite (memPartition f n) := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [memPartition_succ]
    have : Finite (memPartition f n) := Set.finite_coe_iff.mp ih
    rw [← Set.finite_coe_iff]
    simp_rw [setOf_exists, ← exists_prop, setOf_exists, setOf_or]
    refine Finite.Set.finite_biUnion (memPartition f n) _ (fun u _ ↦ ?_)
    rw [Set.finite_coe_iff]
    simp

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