nonempty_coe_sort — Mathlib

English

A subset s of α has a nonempty carrier; equivalently, the subtype {x ∈ α | x ∈ s} is nonempty iff s is nonempty.

Русский

Пусть S — подмножество α. Тогда непустость множества {x ∈ α | x ∈ s} эквивалентна непустости S.

LaTeX

$$$ \text{Nonempty}({x : \alpha \mid x \in s}) \iff \exists x \in s$$$

Lean4

theorem nonempty_coe_sort {s : Set α} : Nonempty ↥s ↔ s.Nonempty :=
  nonempty_subtype

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