mem_iff_nonempty — Mathlib

English

Let α be a Subsingleton type. Then for any s ⊆ α and any x ∈ α, x ∈ s ↔ s.Nonempty.

Русский

Пусть α — однопредметный тип. Тогда для любого s ⊆ α и любого x ∈ α, x ∈ s ⇔ s.Nonempty.

LaTeX

$$$ x \\in s \\iff s.Nonempty $$$

Lean4

theorem mem_iff_nonempty {α : Type*} [Subsingleton α] {s : Set α} {x : α} : x ∈ s ↔ s.Nonempty :=
  ⟨fun hx => ⟨x, hx⟩, fun ⟨y, hy⟩ => Subsingleton.elim y x ▸ hy⟩

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