memPartitionSet_mem — Mathlib

English

By induction, the block memPartitionSet(f,n,a) belongs to memPartition(f,n).

Русский

По индукции блок memPartitionSet(f,n,a) принадлежит memPartition(f,n).

LaTeX

$$$\\operatorname{memPartitionSet}(f,n,a) \\in \\operatorname{memPartition}(f,n).$$$

Lean4

theorem memPartitionSet_mem (f : ℕ → Set α) (n : ℕ) (a : α) : memPartitionSet f n a ∈ memPartition f n := by
  induction n with
  | zero => simp [memPartitionSet]
  | succ n ih =>
    classical
    rw [memPartitionSet_succ, memPartition_succ]
    refine ⟨memPartitionSet f n a, ?_⟩
    split_ifs <;> simp [ih]

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