atomise_empty — Mathlib

English

If s is nonempty, atomise(s, ∅) produces a single block equal to s.

Русский

Если s непусто, атомизация atomise(s, ∅) даёт одно блок-ядро, равное s.

LaTeX

$$$(atomise(s,\\varnothing)).parts = \\{s\\}$, \\quad s \\neq \\varnothing$$$

Lean4

theorem atomise_empty (hs : s.Nonempty) : (atomise s ∅).parts = { s } :=
  by
  simp only [atomise, powerset_empty, image_singleton, notMem_empty, IsEmpty.forall_iff, imp_true_iff, filter_true]
  exact erase_eq_of_notMem (notMem_singleton.2 hs.ne_empty.symm)

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