memPartitionSet_of_mem — Mathlib

English

If s ∈ memPartition(f,n) and a ∈ s, then memPartitionSet(f,n,a) = s.

Русский

Если s ∈ memPartition(f,n) и a ∈ s, то memPartitionSet(f,n,a) = s.

LaTeX

$$$\\{f : \\mathbb{N} \\to \\mathcal{P}(\\alpha)\\} \\Rightarrow \\forall (f)(n)(a)(s: Set\\alpha), \\ s \\in \\operatorname{memPartition}(f,n) \\land a \\in s \\Rightarrow \\operatorname{memPartitionSet}(f,n,a) = s$$$

Lean4

theorem memPartitionSet_of_mem {f : ℕ → Set α} {n : ℕ} {a : α} {s : Set α} (hs : s ∈ memPartition f n) (ha : a ∈ s) :
    memPartitionSet f n a = s :=
  (memPartitionSet_eq_iff a hs).mpr ha

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