not_subset_singleton — Mathlib

English

If a Finite nontrivial s is not contained in any singleton {a}, i.e., s is not a subset of {a} for any a.

Русский

Если Finset s не тривиален, то для любого элемента a верно, что s не является подмножество {a}.

LaTeX

$$$s\text{ Nontrivial} \Rightarrow \forall a, \lnot (s \subseteq \{a\})$$$

Lean4

theorem not_subset_singleton (hs : s.Nontrivial) : ¬s ⊆ { a } :=
  mod_cast hs.coe.not_subset_singleton

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