instFintypeFinset — Mathlib

English

If b ∈ (P.bind Q).parts, then there exists A ∈ P.parts such that b ∈ (Q A hA).parts.

Русский

Если b принадлежит частям z связки P.bind Q, существует A ∈ P.parts, для которого b принадлежит частям (Q A hA).

LaTeX

$$$b \in (P.bind Q).parts \iff \exists A \in P.parts, b \in (Q A A.2).parts$$$

Lean4

instance [DecidableEq α] {s : Finset α} : Fintype (Finpartition s)
    where
  elems :=
    s.powerset.powerset.image fun ps ↦
      if h : ps.sup id = s ∧ ⊥ ∉ ps ∧ ps.SupIndep id then ⟨ps, h.2.2, h.1, h.2.1⟩ else ⊤
  complete
    P := by
    refine mem_image.mpr ⟨P.parts, ?_, ?_⟩
    · rw [mem_powerset]; intro p hp; rw [mem_powerset]; exact P.le hp
    · simp [P.supIndep, P.sup_parts, P.bot_notMem, -bot_eq_empty]

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