Theorems · Definition

Equiv.subtypeUnivEquiv

{α : Sort u_9} → {p : α → Prop} → (∀ (x : α), p x) → Subtype p ≃ α

If a proposition holds for all elements, then the subtype is equivalent to the original type.

Defined in

Mathlib.Logic.Equiv.Basic

Cited by

11 results in Mathlib

Foundations

Depth 10 from the axioms · uses no axioms