Documentation

Mathlib.Init.Data.Subtype.Basic

Subtypes #

These are ported from the Lean 3 standard library file init/data/subtype/basic.lean.

theorem Subtype.exists_of_subtype {α : Type u} {p : αProp} :
{ x // p x }x, p x
theorem Subtype.tag_irrelevant {α : Type u} {p : αProp} {a : α} (h1 : p a) (h2 : p a) :
{ val := a, property := h1 } = { val := a, property := h2 }
theorem Subtype.ne_of_val_ne {α : Type u} {p : αProp} {a1 : { x // p x }} {a2 : { x // p x }} :
a1.val a2.vala1 a2
def Subtype.inhabited {α : Type u} {p : αProp} {a : α} (h : p a) :
Inhabited { x // p x }

If there is some element satisfying the predicate, then the subtype is inhabited.

Equations
Instances For