nonempty_of_mem_partition — Mathlib

English

If c is a partition of α, then every member s ∈ c is nonempty.

Русский

Если c является разбиением α, то каждый элемент s ∈ c непуст.

LaTeX

$$$\\\\forall s \\\\in c, \\\\ s \\\\neq \\\\emptyset$$$

Lean4

/-- A partition of `α` does not contain the empty set. -/
theorem nonempty_of_mem_partition {c : Set (Set α)} (hc : IsPartition c) {s} (h : s ∈ c) : s.Nonempty :=
  Set.nonempty_iff_ne_empty.2 fun hs0 => hc.1 <| hs0 ▸ h

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