nontrivial_coe — Mathlib

English

For a finite set s, the nontriviality of the set viewed as a ordinary set is equivalent to the nontriviality of the finite set s itself.

Русский

Для конечного множества s неравенство не тривиальности сохраняется при переходе к множеству выше уровня; то есть не тривиальность «множества» совпадает с не тривиальностью самого множества.

LaTeX

$$$(s : Set\,\alpha).Nontrivial \iff s.Nontrivial$$$

Lean4

@[simp, norm_cast]
theorem nontrivial_coe : (s : Set α).Nontrivial ↔ s.Nontrivial :=
  .rfl

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