mem_bot_iff — Mathlib

English

An element t is a block in the bottom partition of s exactly when t is a singleton {a} for some a ∈ s.

Русский

Элемент t является блоком в нижнем разбиении s тогда и только тогда, когда t = {a} для некоторого a ∈ s.

LaTeX

$$$ t \\in (\\perp_{Finpartition(s)}).\\mathrm{parts} \\;\\iff\\; \\exists a\\in s, \\{a\\} = t$$$

Lean4

theorem mem_bot_iff : t ∈ (⊥ : Finpartition s).parts ↔ ∃ a ∈ s, { a } = t :=
  mem_map

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