unique_subtype_iff_existsUnique — Mathlib

English

Nonempty (Unique (Subtype p)) iff ExistsUnique a with p(a).

Русский

Nonempty (Unique (Subtype p)) эквивалентно ExistsUnique a: p(a).

LaTeX

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

Lean4

theorem unique_subtype_iff_existsUnique {α} (p : α → Prop) : Nonempty (Unique (Subtype p)) ↔ ∃! a, p a :=
  ⟨fun ⟨u⟩ ↦ ⟨u.default.1, u.default.2, fun a h ↦ congr_arg Subtype.val (u.uniq ⟨a, h⟩)⟩, fun ⟨a, ha, he⟩ ↦
    ⟨⟨⟨⟨a, ha⟩⟩, fun ⟨b, hb⟩ ↦ by
        congr
        exact he b hb⟩⟩⟩

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