nonempty_subtype — Mathlib

English

The subtype {x : α | p x} is nonempty iff there exists an a : α with p a.

Русский

Подтип {x : α | p x} непуст тогда, когда существует a : α такой, что p a.

LaTeX

$$$\operatorname{Nonempty}(\mathrm{Subtype}\,p) \iff \exists a : \alpha, p(a)$$$

Lean4

@[simp]
theorem nonempty_subtype {α} {p : α → Prop} : Nonempty (Subtype p) ↔ ∃ a : α, p a :=
  Iff.intro (fun ⟨⟨a, h⟩⟩ ↦ ⟨a, h⟩) fun ⟨a, h⟩ ↦ ⟨⟨a, h⟩⟩

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