mem_ofWithBot — Mathlib

English

Membership in the built prepartition equals membership of the corresponding WithBot box in the original set.

Русский

Принадлежность к построенному предразбиению равна принадлежности соответствующей коробке WithBot в исходном множестве.

LaTeX

$$$ J \\in (ofWithBot boxes \\; le\_of\_mem \\; pairwise\\_disjoint) \\iff (J : WithBot (Box ι)) \\in boxes $$$

Lean4

@[simp]
theorem mem_ofWithBot {boxes : Finset (WithBot (Box ι))} {h₁ h₂} :
    J ∈ (ofWithBot boxes h₁ h₂ : Prepartition I) ↔ (J : WithBot (Box ι)) ∈ boxes :=
  mem_eraseNone

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