noncomputable def
Classical.indefiniteDescription
{α : Sort u}
(p : α → Prop)
(h : ∃ x, p x)
:
{ x // p x }
Equations
- Classical.indefiniteDescription p h = Classical.choice (_ : Nonempty { x // p x })
Equations
- Classical.choose h = (Classical.indefiniteDescription p h).val
Equations
- Classical.inhabited_of_nonempty h = { default := Classical.choice h }
Equations
Equations
- Classical.propDecidable a = Classical.choice (_ : Nonempty (Decidable a))
Equations
- Classical.decidableInhabited a = { default := inferInstance }
Equations
- Classical.typeDecidableEq α x y = inferInstance
Equations
- Classical.typeDecidable α = match Classical.propDecidable (Nonempty α) with | isTrue hp => PSum.inl default | isFalse hn => PSum.inr (_ : α → False)
noncomputable def
Classical.strongIndefiniteDescription
{α : Sort u}
(p : α → Prop)
(h : Nonempty α)
:
{ x // (∃ y, p y) → p x }
Equations
- Classical.strongIndefiniteDescription p h = if hp : ∃ x, p x then let_fun this := let xp := Classical.indefiniteDescription (fun x => p x) hp; { val := xp.val, property := Classical.strongIndefiniteDescription.proof_1 p hp }; this else { val := Classical.choice h, property := Classical.strongIndefiniteDescription.proof_2 p h hp }
Equations
- Classical.epsilon p = (Classical.strongIndefiniteDescription p h).val
theorem
Classical.epsilon_spec_aux
{α : Sort u}
(h : Nonempty α)
(p : α → Prop)
:
(∃ y, p y) → p (Classical.epsilon p)
theorem
Classical.epsilon_spec
{α : Sort u}
{p : α → Prop}
(hex : ∃ y, p y)
:
p (Classical.epsilon p)
theorem
Classical.axiomOfChoice
{α : Sort u}
{β : α → Sort v}
{r : (x : α) → β x → Prop}
(h : ∀ (x : α), ∃ y, r x y)
:
∃ f, (x : α) → r x (f x)
theorem
Classical.skolem
{α : Sort u}
{b : α → Sort v}
{p : (x : α) → b x → Prop}
:
(∀ (x : α), ∃ y, p x y) ↔ ∃ f, (x : α) → p x (f x)
Equations
- Classical.«tacticByCases__:_» = Lean.ParserDescr.node `Classical.«tacticByCases__:_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.nonReservedSymbol "byCases" false) (Lean.ParserDescr.const `ident)) (Lean.ParserDescr.symbol ":")) (Lean.ParserDescr.cat `term 0))