Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+πŸ–±οΈto focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-/
import Std.Tactic.Ext
import Std.Tactic.Lint.Basic
import Std.Logic
import Std.WF
import Mathlib.Tactic.Alias
import Mathlib.Tactic.Basic
import Mathlib.Tactic.Relation.Rfl
import Mathlib.Tactic.Relation.Symm
import Mathlib.Mathport.Attributes
import Mathlib.Mathport.Rename
import Mathlib.Tactic.Relation.Trans

#align opt_param_eq 
optParam_eq: βˆ€ (Ξ± : Sort u) (default : Ξ±), optParam Ξ± default = Ξ±
optParam_eq
/- Implication -/ @[deprecated] def
Implies: Prop β†’ Prop β†’ Prop
Implies
(
a: Prop
a
b: Prop
b
:
Prop: Type
Prop
) :=
a: Prop
a
β†’
b: Prop
b
/-- Implication `β†’` is transitive. If `P β†’ Q` and `Q β†’ R` then `P β†’ R`. -/ -- FIXME This should have `@[trans]`, but the `trans` attribute PR'd in #253 rejects it. -- Note that it is still rejected after #857. @[deprecated] theorem
Implies.trans: βˆ€ {p q r : Prop}, (p β†’ q) β†’ (q β†’ r) β†’ p β†’ r
Implies.trans
{
p: Prop
p
q: Prop
q
r: Prop
r
:
Prop: Type
Prop
} (
h₁: p β†’ q
h₁
:
p: Prop
p
β†’
q: Prop
q
) (
hβ‚‚: q β†’ r
hβ‚‚
:
q: Prop
q
β†’
r: Prop
r
) :
p: Prop
p
β†’
r: Prop
r
:= fun
hp: ?m.48
hp
↦
hβ‚‚: q β†’ r
hβ‚‚
(
h₁: p β†’ q
h₁
hp: ?m.48
hp
) /- Not -/ @[deprecated] def
NonContradictory: Prop β†’ Prop
NonContradictory
(
a: Prop
a
:
Prop: Type
Prop
) :
Prop: Type
Prop
:= ¬¬
a: Prop
a
#align non_contradictory_intro
not_not_intro: βˆ€ {p : Prop}, p β†’ ¬¬p
not_not_intro
/- Eq -/ alias
proofIrrel: βˆ€ {a : Prop} (h₁ hβ‚‚ : a), h₁ = hβ‚‚
proofIrrel
←
proof_irrel: βˆ€ {a : Prop} (h₁ hβ‚‚ : a), h₁ = hβ‚‚
proof_irrel
alias
congrFun: βˆ€ {Ξ± : Sort u} {Ξ² : Ξ± β†’ Sort v} {f g : (x : Ξ±) β†’ Ξ² x}, f = g β†’ βˆ€ (a : Ξ±), f a = g a
congrFun
←
congr_fun: βˆ€ {Ξ± : Sort u} {Ξ² : Ξ± β†’ Sort v} {f g : (x : Ξ±) β†’ Ξ² x}, f = g β†’ βˆ€ (a : Ξ±), f a = g a
congr_fun
alias
congrArg: βˆ€ {Ξ± : Sort u} {Ξ² : Sort v} {a₁ aβ‚‚ : Ξ±} (f : Ξ± β†’ Ξ²), a₁ = aβ‚‚ β†’ f a₁ = f aβ‚‚
congrArg
←
congr_arg: βˆ€ {Ξ± : Sort u} {Ξ² : Sort v} {a₁ aβ‚‚ : Ξ±} (f : Ξ± β†’ Ξ²), a₁ = aβ‚‚ β†’ f a₁ = f aβ‚‚
congr_arg
@[deprecated] theorem
trans_rel_left: βˆ€ {Ξ± : Sort u} {a b c : Ξ±} (r : Ξ± β†’ Ξ± β†’ Prop), r a b β†’ b = c β†’ r a c
trans_rel_left
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
a: Ξ±
a
b: Ξ±
b
c: Ξ±
c
:
Ξ±: Sort u
Ξ±
} (
r: Ξ± β†’ Ξ± β†’ Prop
r
:
Ξ±: Sort u
Ξ±
β†’
Ξ±: Sort u
Ξ±
β†’
Prop: Type
Prop
) (
h₁: r a b
h₁
:
r: Ξ± β†’ Ξ± β†’ Prop
r
a: Ξ±
a
b: Ξ±
b
) (
hβ‚‚: b = c
hβ‚‚
:
b: Ξ±
b
=
c: Ξ±
c
) :
r: Ξ± β†’ Ξ± β†’ Prop
r
a: Ξ±
a
c: Ξ±
c
:=
hβ‚‚: b = c
hβ‚‚
β–Έ
h₁: r a b
h₁
@[deprecated] theorem
trans_rel_right: βˆ€ {Ξ± : Sort u} {a b c : Ξ±} (r : Ξ± β†’ Ξ± β†’ Prop), a = b β†’ r b c β†’ r a c
trans_rel_right
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
a: Ξ±
a
b: Ξ±
b
c: Ξ±
c
:
Ξ±: Sort u
Ξ±
} (
r: Ξ± β†’ Ξ± β†’ Prop
r
:
Ξ±: Sort u
Ξ±
β†’
Ξ±: Sort u
Ξ±
β†’
Prop: Type
Prop
) (
h₁: a = b
h₁
:
a: Ξ±
a
=
b: Ξ±
b
) (
hβ‚‚: r b c
hβ‚‚
:
r: Ξ± β†’ Ξ± β†’ Prop
r
b: Ξ±
b
c: Ξ±
c
) :
r: Ξ± β†’ Ξ± β†’ Prop
r
a: Ξ±
a
c: Ξ±
c
:=
h₁: a = b
h₁
β–Έ
hβ‚‚: r b c
hβ‚‚
theorem
not_of_eq_false: βˆ€ {p : Prop}, p = False β†’ Β¬p
not_of_eq_false
{
p: Prop
p
:
Prop: Type
Prop
} (
h: p = False
h
:
p: Prop
p
=
False: Prop
False
) : Β¬
p: Prop
p
:= fun
hp: ?m.171
hp
↦
h: p = False
h
β–Έ
hp: ?m.171
hp
theorem
cast_proof_irrel: βˆ€ {Ξ± Ξ² : Sort u_1} (h₁ hβ‚‚ : Ξ± = Ξ²) (a : Ξ±), cast h₁ a = cast hβ‚‚ a
cast_proof_irrel
(
h₁: Ξ± = Ξ²
h₁
hβ‚‚: Ξ± = Ξ²
hβ‚‚
:
Ξ±: ?m.188
Ξ±
=
Ξ²: ?m.193
Ξ²
) (
a: Ξ±
a
:
Ξ±: ?m.188
Ξ±
) :
cast: {Ξ± Ξ² : Sort ?u.209} β†’ Ξ± = Ξ² β†’ Ξ± β†’ Ξ²
cast
h₁: Ξ± = Ξ²
h₁
a: Ξ±
a
=
cast: {Ξ± Ξ² : Sort ?u.218} β†’ Ξ± = Ξ² β†’ Ξ± β†’ Ξ²
cast
hβ‚‚: Ξ± = Ξ²
hβ‚‚
a: Ξ±
a
:=
rfl: βˆ€ {Ξ± : Sort ?u.231} {a : Ξ±}, a = a
rfl
attribute [symm]
Eq.symm: βˆ€ {Ξ± : Sort u} {a b : Ξ±}, a = b β†’ b = a
Eq.symm
/- Ne -/ theorem
Ne.def: βˆ€ {Ξ± : Sort u} (a b : Ξ±), (a β‰  b) = Β¬a = b
Ne.def
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} (
a: Ξ±
a
b: Ξ±
b
:
Ξ±: Sort u
Ξ±
) : (
a: Ξ±
a
β‰ 
b: Ξ±
b
) = Β¬ (
a: Ξ±
a
=
b: Ξ±
b
) :=
rfl: βˆ€ {Ξ± : Sort ?u.268} {a : Ξ±}, a = a
rfl
attribute [symm]
Ne.symm: βˆ€ {Ξ± : Sort u} {a b : Ξ±}, a β‰  b β†’ b β‰  a
Ne.symm
/- HEq -/ alias
eqRec_heq: βˆ€ {Ξ± : Sort u} {Ο† : Ξ± β†’ Sort v} {a a' : Ξ±} (h : a = a') (p : Ο† a), HEq (Eq.recOn h p) p
eqRec_heq
←
eq_rec_heq: βˆ€ {Ξ± : Sort u} {Ο† : Ξ± β†’ Sort v} {a a' : Ξ±} (h : a = a') (p : Ο† a), HEq (Eq.recOn h p) p
eq_rec_heq
-- FIXME This is still rejected after #857 -- attribute [refl] HEq.refl attribute [symm]
HEq.symm: βˆ€ {Ξ± Ξ² : Sort u} {a : Ξ±} {b : Ξ²}, HEq a b β†’ HEq b a
HEq.symm
attribute [trans]
HEq.trans: βˆ€ {Ξ± Ξ² Ο† : Sort u} {a : Ξ±} {b : Ξ²} {c : Ο†}, HEq a b β†’ HEq b c β†’ HEq a c
HEq.trans
attribute [trans]
heq_of_eq_of_heq: βˆ€ {Ξ± Ξ² : Sort u} {a a' : Ξ±} {b : Ξ²}, a = a' β†’ HEq a' b β†’ HEq a b
heq_of_eq_of_heq
theorem
heq_of_eq_rec_left: βˆ€ {Ξ± : Sort u_1} {Ο† : Ξ± β†’ Sort v} {a a' : Ξ±} {p₁ : Ο† a} {pβ‚‚ : Ο† a'} (e : a = a'), e β–Έ p₁ = pβ‚‚ β†’ HEq p₁ pβ‚‚
heq_of_eq_rec_left
{
Ο†: Ξ± β†’ Sort v
Ο†
:
Ξ±: ?m.311
Ξ±
β†’
Sort v: Type v
Sort
Sort v: Type v
v
} {
a: Ξ±
a
a': Ξ±
a'
:
Ξ±: ?m.311
Ξ±
} {
p₁: Ο† a
p₁
:
Ο†: Ξ± β†’ Sort v
Ο†
a: Ξ±
a
} {
pβ‚‚: Ο† a'
pβ‚‚
:
Ο†: Ξ± β†’ Sort v
Ο†
a': Ξ±
a'
} : (
e: a = a'
e
:
a: Ξ±
a
=
a': Ξ±
a'
) β†’ (
hβ‚‚: e β–Έ p₁ = pβ‚‚
hβ‚‚
:
Eq.rec: {Ξ± : Sort ?u.333} β†’ {a : Ξ±} β†’ {motive : (a_1 : Ξ±) β†’ a = a_1 β†’ Sort ?u.334} β†’ motive a (_ : a = a) β†’ {a_1 : Ξ±} β†’ (t : a = a_1) β†’ motive a_1 t
Eq.rec
(motive := fun
a: ?m.352
a
_: ?m.355
_
↦
Ο†: Ξ± β†’ Sort v
Ο†
a: ?m.352
a
)
p₁: Ο† a
p₁
e: a = a'
e
=
pβ‚‚: Ο† a'
pβ‚‚
) β†’
HEq: {Ξ± : Sort ?u.369} β†’ Ξ± β†’ {Ξ² : Sort ?u.369} β†’ Ξ² β†’ Prop
HEq
p₁: Ο† a
p₁
pβ‚‚: Ο† a'
pβ‚‚
|
rfl: βˆ€ {Ξ± : Sort ?u.555} {a : Ξ±}, a = a
rfl
,
rfl: βˆ€ {Ξ± : Sort ?u.559} {a : Ξ±}, a = a
rfl
=>
HEq.rfl: βˆ€ {Ξ± : Sort ?u.603} {a : Ξ±}, HEq a a
HEq.rfl
theorem
heq_of_eq_rec_right: βˆ€ {Ξ± : Sort u_1} {Ο† : Ξ± β†’ Sort v} {a a' : Ξ±} {p₁ : Ο† a} {pβ‚‚ : Ο† a'} (e : a' = a), p₁ = e β–Έ pβ‚‚ β†’ HEq p₁ pβ‚‚
heq_of_eq_rec_right
{
Ο†: Ξ± β†’ Sort v
Ο†
:
Ξ±: ?m.905
Ξ±
β†’
Sort v: Type v
Sort
Sort v: Type v
v
} {
a: Ξ±
a
a': Ξ±
a'
:
Ξ±: ?m.905
Ξ±
} {
p₁: Ο† a
p₁
:
Ο†: Ξ± β†’ Sort v
Ο†
a: Ξ±
a
} {
pβ‚‚: Ο† a'
pβ‚‚
:
Ο†: Ξ± β†’ Sort v
Ο†
a': Ξ±
a'
} : (
e: a' = a
e
:
a': Ξ±
a'
=
a: Ξ±
a
) β†’ (
hβ‚‚: p₁ = e β–Έ pβ‚‚
hβ‚‚
:
p₁: Ο† a
p₁
=
Eq.rec: {Ξ± : Sort ?u.927} β†’ {a : Ξ±} β†’ {motive : (a_1 : Ξ±) β†’ a = a_1 β†’ Sort ?u.928} β†’ motive a (_ : a = a) β†’ {a_1 : Ξ±} β†’ (t : a = a_1) β†’ motive a_1 t
Eq.rec
(motive := fun
a: ?m.946
a
_: ?m.949
_
↦
Ο†: Ξ± β†’ Sort v
Ο†
a: ?m.946
a
)
pβ‚‚: Ο† a'
pβ‚‚
e: a' = a
e
) β†’
HEq: {Ξ± : Sort ?u.963} β†’ Ξ± β†’ {Ξ² : Sort ?u.963} β†’ Ξ² β†’ Prop
HEq
p₁: Ο† a
p₁
pβ‚‚: Ο† a'
pβ‚‚
|
rfl: βˆ€ {Ξ± : Sort u_1} {a : Ξ±}, a = a
rfl
,
rfl: βˆ€ {Ξ± : Sort ?u.1153} {a : Ξ±}, a = a
rfl
=>
HEq.rfl: βˆ€ {Ξ± : Sort ?u.1196} {a : Ξ±}, HEq a a
HEq.rfl
theorem
of_heq_true: βˆ€ {a : Prop}, HEq a True β†’ a
of_heq_true
{
a: Prop
a
:
Prop: Type
Prop
} (
h: HEq a True
h
:
HEq: {Ξ± : Sort ?u.1498} β†’ Ξ± β†’ {Ξ² : Sort ?u.1498} β†’ Ξ² β†’ Prop
HEq
a: Prop
a
True: Prop
True
) :
a: Prop
a
:=
of_eq_true: βˆ€ {p : Prop}, p = True β†’ p
of_eq_true
(
eq_of_heq: βˆ€ {Ξ± : Sort ?u.1507} {a a' : Ξ±}, HEq a a' β†’ a = a'
eq_of_heq
h: HEq a True
h
) theorem
eq_rec_compose: βˆ€ {Ξ± Ξ² Ο† : Sort u} (p₁ : Ξ² = Ο†) (pβ‚‚ : Ξ± = Ξ²) (a : Ξ±), Eq.recOn p₁ (Eq.recOn pβ‚‚ a) = Eq.recOn (_ : Ξ± = Ο†) a
eq_rec_compose
{
Ξ±: Sort u
Ξ±
Ξ²: Sort u
Ξ²
Ο†: Sort u
Ο†
:
Sort u: Type u
Sort
Sort u: Type u
u
} : βˆ€ (
p₁: Ξ² = Ο†
p₁
:
Ξ²: Sort u
Ξ²
=
Ο†: Sort u
Ο†
) (
pβ‚‚: Ξ± = Ξ²
pβ‚‚
:
Ξ±: Sort u
Ξ±
=
Ξ²: Sort u
Ξ²
) (
a: Ξ±
a
:
Ξ±: Sort u
Ξ±
), (
Eq.recOn: {Ξ± : Sort ?u.1540} β†’ {a : Ξ±} β†’ {motive : (a_1 : Ξ±) β†’ a = a_1 β†’ Sort ?u.1541} β†’ {a_1 : Ξ±} β†’ (t : a = a_1) β†’ motive a (_ : a = a) β†’ motive a_1 t
Eq.recOn
p₁: Ξ² = Ο†
p₁
(
Eq.recOn: {Ξ± : Sort ?u.1578} β†’ {a : Ξ±} β†’ {motive : (a_1 : Ξ±) β†’ a = a_1 β†’ Sort ?u.1579} β†’ {a_1 : Ξ±} β†’ (t : a = a_1) β†’ motive a (_ : a = a) β†’ motive a_1 t
Eq.recOn
pβ‚‚: Ξ± = Ξ²
pβ‚‚
a: Ξ±
a
:
Ξ²: Sort u
Ξ²
) :
Ο†: Sort u
Ο†
) =
Eq.recOn: {Ξ± : Sort ?u.1648} β†’ {a : Ξ±} β†’ {motive : (a_1 : Ξ±) β†’ a = a_1 β†’ Sort ?u.1649} β†’ {a_1 : Ξ±} β†’ (t : a = a_1) β†’ motive a (_ : a = a) β†’ motive a_1 t
Eq.recOn
(
Eq.trans: βˆ€ {Ξ± : Sort ?u.1674} {a b c : Ξ±}, a = b β†’ b = c β†’ a = c
Eq.trans
pβ‚‚: Ξ± = Ξ²
pβ‚‚
p₁: Ξ² = Ο†
p₁
)
a: Ξ±
a
|
rfl: βˆ€ {Ξ± : Sort ?u.2023} {a : Ξ±}, a = a
rfl
,
rfl: βˆ€ {Ξ± : Sort ?u.2027} {a : Ξ±}, a = a
rfl
, _ =>
rfl: βˆ€ {Ξ± : Sort ?u.2072} {a : Ξ±}, a = a
rfl
/- and -/ variable {
a: Prop
a
b: Prop
b
c: Prop
c
d: Prop
d
:
Prop: Type
Prop
} #align and.symm
And.symm: βˆ€ {a b : Prop}, a ∧ b β†’ b ∧ a
And.symm
#align and.swap
And.symm: βˆ€ {a b : Prop}, a ∧ b β†’ b ∧ a
And.symm
/- or -/ #align non_contradictory_em
not_not_em: βˆ€ (a : Prop), ¬¬(a ∨ Β¬a)
not_not_em
#align or.symm
Or.symm: βˆ€ {a b : Prop}, a ∨ b β†’ b ∨ a
Or.symm
#align or.swap
Or.symm: βˆ€ {a b : Prop}, a ∨ b β†’ b ∨ a
Or.symm
/- xor -/ def
Xor': (a b : Prop) β†’ ?m.2374 a b
Xor'
(
a: Prop
a
b: Prop
b
:
Prop: Type
Prop
) := (
a: Prop
a
∧ ¬
b: Prop
b
) ∨ (
b: Prop
b
∧ ¬
a: Prop
a
) #align xor
Xor': Prop β†’ Prop β†’ Prop
Xor'
/- iff -/ #align iff.mp
Iff.mp: βˆ€ {a b : Prop}, (a ↔ b) β†’ a β†’ b
Iff.mp
#align iff.elim_left
Iff.mp: βˆ€ {a b : Prop}, (a ↔ b) β†’ a β†’ b
Iff.mp
#align iff.mpr
Iff.mpr: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
Iff.mpr
#align iff.elim_right
Iff.mpr: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
Iff.mpr
attribute [refl]
Iff.refl: βˆ€ (a : Prop), a ↔ a
Iff.refl
attribute [trans]
Iff.trans: βˆ€ {a b c : Prop}, (a ↔ b) β†’ (b ↔ c) β†’ (a ↔ c)
Iff.trans
attribute [symm]
Iff.symm: βˆ€ {a b : Prop}, (a ↔ b) β†’ (b ↔ a)
Iff.symm
-- This is needed for `calc` to work with `iff`.
instance: Trans Iff Iff Iff
instance
:
Trans: {Ξ± : Sort ?u.2406} β†’ {Ξ² : Sort ?u.2405} β†’ {Ξ³ : Sort ?u.2404} β†’ (Ξ± β†’ Ξ² β†’ Sort ?u.2409) β†’ (Ξ² β†’ Ξ³ β†’ Sort ?u.2408) β†’ outParam (Ξ± β†’ Ξ³ β†’ Sort ?u.2407) β†’ Sort (max(max(max(max(max(max1?u.2409)?u.2406)?u.2405)?u.2404)?u.2408)?u.2407)
Trans
Iff: Prop β†’ Prop β†’ Prop
Iff
Iff: Prop β†’ Prop β†’ Prop
Iff
Iff: Prop β†’ Prop β†’ Prop
Iff
where trans := fun
p: ?m.2468
p
q: ?m.2471
q
↦
p: ?m.2468
p
.
trans: βˆ€ {a b c : Prop}, (a ↔ b) β†’ (b ↔ c) β†’ (a ↔ c)
trans
q: ?m.2471
q
#align not_congr
not_congr: βˆ€ {a b : Prop}, (a ↔ b) β†’ (Β¬a ↔ Β¬b)
not_congr
#align not_iff_not_of_iff
not_congr: βˆ€ {a b : Prop}, (a ↔ b) β†’ (Β¬a ↔ Β¬b)
not_congr
#align not_non_contradictory_iff_absurd
not_not_not: βˆ€ {a : Prop}, ¬¬¬a ↔ Β¬a
not_not_not
alias
not_not_not: βˆ€ {a : Prop}, ¬¬¬a ↔ Β¬a
not_not_not
↔
not_of_not_not_not: βˆ€ {a : Prop}, ¬¬¬a β†’ Β¬a
not_of_not_not_not
_ -- FIXME -- attribute [congr] not_congr @[deprecated
and_comm: βˆ€ {a b : Prop}, a ∧ b ↔ b ∧ a
and_comm
] theorem
and_comm': βˆ€ (a b : Prop), a ∧ b ↔ b ∧ a
and_comm'
(
a: Prop
a
b: ?m.2631
b
) :
a: ?m.2628
a
∧
b: ?m.2631
b
↔
b: ?m.2631
b
∧
a: ?m.2628
a
:=
and_comm: βˆ€ {a b : Prop}, a ∧ b ↔ b ∧ a
and_comm
#align and.comm
and_comm: βˆ€ {a b : Prop}, a ∧ b ↔ b ∧ a
and_comm
#align and_comm
and_comm': βˆ€ (a b : Prop), a ∧ b ↔ b ∧ a
and_comm'
@[deprecated
and_assoc: βˆ€ {a b c : Prop}, (a ∧ b) ∧ c ↔ a ∧ b ∧ c
and_assoc
] theorem
and_assoc': βˆ€ (a b : Prop), (a ∧ b) ∧ c ↔ a ∧ b ∧ c
and_assoc'
(
a: ?m.2654
a
b: Prop
b
) : (
a: ?m.2654
a
∧
b: ?m.2657
b
) ∧
c: Prop
c
↔
a: ?m.2654
a
∧ (
b: ?m.2657
b
∧
c: Prop
c
) :=
and_assoc: βˆ€ {a b c : Prop}, (a ∧ b) ∧ c ↔ a ∧ b ∧ c
and_assoc
#align and_assoc
and_assoc': βˆ€ {c : Prop} (a b : Prop), (a ∧ b) ∧ c ↔ a ∧ b ∧ c
and_assoc'
#align and.assoc
and_assoc: βˆ€ {a b c : Prop}, (a ∧ b) ∧ c ↔ a ∧ b ∧ c
and_assoc
#align and.left_comm
and_left_comm: βˆ€ {a b c : Prop}, a ∧ b ∧ c ↔ b ∧ a ∧ c
and_left_comm
#align and_iff_left
and_iff_leftβ‚“: βˆ€ {b a : Prop}, b β†’ (a ∧ b ↔ a)
and_iff_leftβ‚“
-- reorder implicits variable (
p: ?m.2789
p
) -- FIXME: remove _iff and add _eq for the lean 4 core versions theorem
and_true_iff: p ∧ True ↔ p
and_true_iff
:
p: ?m.2693
p
∧
True: Prop
True
↔
p: ?m.2693
p
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
and_true: βˆ€ (p : Prop), (p ∧ True) = p
and_true
_: Prop
_
) #align and_true
and_true_iff: βˆ€ (p : Prop), p ∧ True ↔ p
and_true_iff
theorem
true_and_iff: True ∧ p ↔ p
true_and_iff
:
True: Prop
True
∧
p: ?m.2717
p
↔
p: ?m.2717
p
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
true_and: βˆ€ (p : Prop), (True ∧ p) = p
true_and
_: Prop
_
) #align true_and
true_and_iff: βˆ€ (p : Prop), True ∧ p ↔ p
true_and_iff
theorem
and_false_iff: βˆ€ (p : Prop), p ∧ False ↔ False
and_false_iff
:
p: ?m.2741
p
∧
False: Prop
False
↔
False: Prop
False
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
and_false: βˆ€ (p : Prop), (p ∧ False) = False
and_false
_: Prop
_
) #align and_false
and_false_iff: βˆ€ (p : Prop), p ∧ False ↔ False
and_false_iff
theorem
false_and_iff: βˆ€ (p : Prop), False ∧ p ↔ False
false_and_iff
:
False: Prop
False
∧
p: ?m.2765
p
↔
False: Prop
False
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
false_and: βˆ€ (p : Prop), (False ∧ p) = False
false_and
_: Prop
_
) #align false_and
false_and_iff: βˆ€ (p : Prop), False ∧ p ↔ False
false_and_iff
#align not_and_self
not_and_self_iff: βˆ€ (a : Prop), Β¬a ∧ a ↔ False
not_and_self_iff
#align and_not_self
and_not_self_iff: βˆ€ (a : Prop), a ∧ Β¬a ↔ False
and_not_self_iff
theorem
and_self_iff: p ∧ p ↔ p
and_self_iff
:
p: ?m.2789
p
∧
p: ?m.2789
p
↔
p: ?m.2789
p
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
and_self: βˆ€ (p : Prop), (p ∧ p) = p
and_self
_: Prop
_
) #align and_self
and_self_iff: βˆ€ (p : Prop), p ∧ p ↔ p
and_self_iff
#align or.imp
Or.impβ‚“: βˆ€ {a c b d : Prop}, (a β†’ c) β†’ (b β†’ d) β†’ a ∨ b β†’ c ∨ d
Or.impβ‚“
-- reorder implicits #align and.elim
And.elimβ‚“: {a b : Prop} β†’ {Ξ± : Sort u_1} β†’ (a β†’ b β†’ Ξ±) β†’ a ∧ b β†’ Ξ±
And.elimβ‚“
#align iff.elim
Iff.elimβ‚“: {a b : Prop} β†’ {Ξ± : Sort u_1} β†’ ((a β†’ b) β†’ (b β†’ a) β†’ Ξ±) β†’ (a ↔ b) β†’ Ξ±
Iff.elimβ‚“
#align imp_congr
imp_congrβ‚“: βˆ€ {a c b d : Prop}, (a ↔ c) β†’ (b ↔ d) β†’ (a β†’ b ↔ c β†’ d)
imp_congrβ‚“
#align imp_congr_ctx
imp_congr_ctxβ‚“: βˆ€ {a c b d : Prop}, (a ↔ c) β†’ (c β†’ (b ↔ d)) β†’ (a β†’ b ↔ c β†’ d)
imp_congr_ctxβ‚“
#align imp_congr_right
imp_congr_rightβ‚“: βˆ€ {a : Sort u_1} {b c : Prop}, (a β†’ (b ↔ c)) β†’ (a β†’ b ↔ a β†’ c)
imp_congr_rightβ‚“
#align eq_true_intro
eq_true: βˆ€ {p : Prop}, p β†’ p = True
eq_true
#align eq_false_intro
eq_false: βˆ€ {p : Prop}, Β¬p β†’ p = False
eq_false
@[deprecated
or_comm: βˆ€ {a b : Prop}, a ∨ b ↔ b ∨ a
or_comm
] theorem
or_comm': βˆ€ (a b : Prop), a ∨ b ↔ b ∨ a
or_comm'
(
a: Prop
a
b: ?m.2819
b
) :
a: ?m.2816
a
∨
b: ?m.2819
b
↔
b: ?m.2819
b
∨
a: ?m.2816
a
:=
or_comm: βˆ€ {a b : Prop}, a ∨ b ↔ b ∨ a
or_comm
#align or.comm
or_comm: βˆ€ {a b : Prop}, a ∨ b ↔ b ∨ a
or_comm
#align or_comm
or_comm': βˆ€ (a b : Prop), a ∨ b ↔ b ∨ a
or_comm'
@[deprecated
or_assoc: βˆ€ {a b c : Prop}, (a ∨ b) ∨ c ↔ a ∨ b ∨ c
or_assoc
] theorem
or_assoc': βˆ€ {c : Prop} (a b : Prop), (a ∨ b) ∨ c ↔ a ∨ b ∨ c
or_assoc'
(
a: Prop
a
b: ?m.2848
b
) : (
a: ?m.2845
a
∨
b: ?m.2848
b
) ∨
c: Prop
c
↔
a: ?m.2845
a
∨ (
b: ?m.2848
b
∨
c: Prop
c
) :=
or_assoc: βˆ€ {a b c : Prop}, (a ∨ b) ∨ c ↔ a ∨ b ∨ c
or_assoc
#align or.assoc
or_assoc: βˆ€ {a b c : Prop}, (a ∨ b) ∨ c ↔ a ∨ b ∨ c
or_assoc
#align or_assoc
or_assoc': βˆ€ {c : Prop} (a b : Prop), (a ∨ b) ∨ c ↔ a ∨ b ∨ c
or_assoc'
#align or_left_comm
or_left_comm: βˆ€ {a b c : Prop}, a ∨ b ∨ c ↔ b ∨ a ∨ c
or_left_comm
#align or.left_comm
or_left_comm: βˆ€ {a b c : Prop}, a ∨ b ∨ c ↔ b ∨ a ∨ c
or_left_comm
#align or_iff_left_of_imp
or_iff_left_of_impβ‚“: βˆ€ {b a : Prop}, (b β†’ a) β†’ (a ∨ b ↔ a)
or_iff_left_of_impβ‚“
-- reorder implicits theorem
true_or_iff: True ∨ p ↔ True
true_or_iff
:
True: Prop
True
∨
p: ?m.2873
p
↔
True: Prop
True
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
true_or: βˆ€ (p : Prop), (True ∨ p) = True
true_or
_: Prop
_
) #align true_or
true_or_iff: βˆ€ (p : Prop), True ∨ p ↔ True
true_or_iff
theorem
or_true_iff: p ∨ True ↔ True
or_true_iff
:
p: ?m.2897
p
∨
True: Prop
True
↔
True: Prop
True
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
or_true: βˆ€ (p : Prop), (p ∨ True) = True
or_true
_: Prop
_
) #align or_true
or_true_iff: βˆ€ (p : Prop), p ∨ True ↔ True
or_true_iff
theorem
false_or_iff: βˆ€ (p : Prop), False ∨ p ↔ p
false_or_iff
:
False: Prop
False
∨
p: ?m.2921
p
↔
p: ?m.2921
p
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
false_or: βˆ€ (p : Prop), (False ∨ p) = p
false_or
_: Prop
_
) #align false_or
false_or_iff: βˆ€ (p : Prop), False ∨ p ↔ p
false_or_iff
theorem
or_false_iff: p ∨ False ↔ p
or_false_iff
:
p: ?m.2945
p
∨
False: Prop
False
↔
p: ?m.2945
p
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
or_false: βˆ€ (p : Prop), (p ∨ False) = p
or_false
_: Prop
_
) #align or_false
or_false_iff: βˆ€ (p : Prop), p ∨ False ↔ p
or_false_iff
theorem
or_self_iff: p ∨ p ↔ p
or_self_iff
:
p: ?m.2969
p
∨
p: ?m.2969
p
↔
p: ?m.2969
p
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
or_self: βˆ€ (p : Prop), (p ∨ p) = p
or_self
_: Prop
_
) #align or_self
or_self_iff: βˆ€ (p : Prop), p ∨ p ↔ p
or_self_iff
theorem
not_or_of_not: βˆ€ {a b : Prop}, Β¬a β†’ Β¬b β†’ Β¬(a ∨ b)
not_or_of_not
: Β¬
a: Prop
a
β†’ Β¬
b: Prop
b
β†’ Β¬(
a: Prop
a
∨
b: Prop
b
) := fun
h1: ?m.3004
h1
h2: ?m.3007
h2
↦
not_or: βˆ€ {p q : Prop}, Β¬(p ∨ q) ↔ Β¬p ∧ Β¬q
not_or
.
2: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
2
⟨
h1: ?m.3004
h1
,
h2: ?m.3007
h2
⟩ #align not_or
not_or_of_not: βˆ€ {a b : Prop}, Β¬a β†’ Β¬b β†’ Β¬(a ∨ b)
not_or_of_not
theorem
iff_true_iff: (a ↔ True) ↔ a
iff_true_iff
: (
a: Prop
a
↔
True: Prop
True
) ↔
a: Prop
a
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
iff_true: βˆ€ (p : Prop), (p ↔ True) = p
iff_true
_: Prop
_
) #align iff_true
iff_true_iff: βˆ€ {a : Prop}, (a ↔ True) ↔ a
iff_true_iff
theorem
true_iff_iff: βˆ€ {a : Prop}, (True ↔ a) ↔ a
true_iff_iff
: (
True: Prop
True
↔
a: Prop
a
) ↔
a: Prop
a
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
true_iff: βˆ€ (p : Prop), (True ↔ p) = p
true_iff
_: Prop
_
) #align true_iff
true_iff_iff: βˆ€ {a : Prop}, (True ↔ a) ↔ a
true_iff_iff
theorem
iff_false_iff: βˆ€ {a : Prop}, (a ↔ False) ↔ Β¬a
iff_false_iff
: (
a: Prop
a
↔
False: Prop
False
) ↔ Β¬
a: Prop
a
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
iff_false: βˆ€ (p : Prop), (p ↔ False) = Β¬p
iff_false
_: Prop
_
) #align iff_false
iff_false_iff: βˆ€ {a : Prop}, (a ↔ False) ↔ Β¬a
iff_false_iff
theorem
false_iff_iff: (False ↔ a) ↔ Β¬a
false_iff_iff
: (
False: Prop
False
↔
a: Prop
a
) ↔ Β¬
a: Prop
a
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
false_iff: βˆ€ (p : Prop), (False ↔ p) = Β¬p
false_iff
_: Prop
_
) #align false_iff
false_iff_iff: βˆ€ {a : Prop}, (False ↔ a) ↔ Β¬a
false_iff_iff
theorem
iff_self_iff: βˆ€ (a : Prop), (a ↔ a) ↔ True
iff_self_iff
(
a: Prop
a
:
Prop: Type
Prop
) : (
a: Prop
a
↔
a: Prop
a
) ↔
True: Prop
True
:=
iff_of_eq: βˆ€ {a b : Prop}, a = b β†’ (a ↔ b)
iff_of_eq
(
iff_self: βˆ€ (p : Prop), (p ↔ p) = True
iff_self
_: Prop
_
) #align iff_self
iff_self_iff: βˆ€ (a : Prop), (a ↔ a) ↔ True
iff_self_iff
#align iff_congr
iff_congrβ‚“: βˆ€ {a c b d : Prop}, (a ↔ c) β†’ (b ↔ d) β†’ ((a ↔ b) ↔ (c ↔ d))
iff_congrβ‚“
-- reorder implicits #align implies_true_iff
imp_true_iff: βˆ€ (Ξ± : Sort u), Ξ± β†’ True ↔ True
imp_true_iff
#align false_implies_iff
false_imp_iff: βˆ€ (a : Prop), False β†’ a ↔ True
false_imp_iff
#align true_implies_iff
true_imp_iff: βˆ€ (Ξ± : Prop), True β†’ Ξ± ↔ Ξ±
true_imp_iff
#align Exists
Exists: {Ξ± : Sort u} β†’ (Ξ± β†’ Prop) β†’ Prop
Exists
-- otherwise it would get the name ExistsCat -- TODO -- attribute [intro] Exists.intro /- exists unique -/ def
ExistsUnique: {Ξ± : Sort ?u.3168} β†’ (p : Ξ± β†’ Prop) β†’ ?m.3173 p
ExistsUnique
(
p: Ξ± β†’ Prop
p
:
Ξ±: ?m.3165
Ξ±
β†’
Prop: Type
Prop
) := βˆƒ
x: ?m.3184
x
,
p: Ξ± β†’ Prop
p
x: ?m.3184
x
∧ βˆ€
y: ?m.3187
y
,
p: Ξ± β†’ Prop
p
y: ?m.3187
y
β†’
y: ?m.3187
y
=
x: ?m.3184
x
open Lean TSyntax.Compat in macro "βˆƒ! "
xs: ?m.3358
xs
:
explicitBinders: ParserDescr
explicitBinders
", "
b: ?m.3346
b
:term : term =>
expandExplicitBinders: Name β†’ Syntax β†’ Syntax β†’ MacroM Syntax
expandExplicitBinders
``
ExistsUnique: {Ξ± : Sort u_1} β†’ (Ξ± β†’ Prop) β†’ Prop
ExistsUnique
xs: ?m.3358
xs
b: ?m.3346
b
/-- Pretty-printing for `ExistsUnique`, following the same pattern as pretty printing for `Exists`. -/ @[app_unexpander
ExistsUnique: {Ξ± : Sort u_1} β†’ (Ξ± β†’ Prop) β†’ Prop
ExistsUnique
] def
unexpandExistsUnique: Lean.PrettyPrinter.Unexpander
unexpandExistsUnique
:
Lean.PrettyPrinter.Unexpander: Type
Lean.PrettyPrinter.Unexpander
| `($(_) fun $
x: ?m.5187
x
:ident ↦ βˆƒ! $
xs: ?m.5180
xs
:binderIdent*, $
b: ?m.5171
b
) => `(βˆƒ! $
x: ?m.5187
x
:ident $
xs: ?m.5180
xs
:binderIdent*, $
b: ?m.5171
b
) | `($(_) fun $
x: ?m.5715
x
:ident ↦ $
b: ?m.5708
b
) => `(βˆƒ! $
x: ?m.6364
x
:ident, $
b: ?m.6357
b
) | `($(_) fun ($
x: ?m.7180
x
:ident : $
t: ?m.7173
t
) ↦ $
b: ?m.7166
b
) => `(βˆƒ! ($
x: ?m.7180
x
:ident : $
t: ?m.7173
t
), $
b: ?m.7166
b
) | _ =>
throw: {Ξ΅ : outParam (Type ?u.7860)} β†’ {m : Type ?u.7859 β†’ Type ?u.7858} β†’ [self : MonadExcept Ξ΅ m] β†’ {Ξ± : Type ?u.7859} β†’ Ξ΅ β†’ m Ξ±
throw
(): Unit
()
-- @[intro] -- TODO theorem
ExistsUnique.intro: βˆ€ {Ξ± : Sort u_1} {p : Ξ± β†’ Prop} (w : Ξ±), p w β†’ (βˆ€ (y : Ξ±), p y β†’ y = w) β†’ βˆƒ! x, p x
ExistsUnique.intro
{
p: Ξ± β†’ Prop
p
:
Ξ±: ?m.24288
Ξ±
β†’
Prop: Type
Prop
} (
w: Ξ±
w
:
Ξ±: ?m.24288
Ξ±
) (
h₁: p w
h₁
:
p: Ξ± β†’ Prop
p
w: Ξ±
w
) (
hβ‚‚: βˆ€ (y : Ξ±), p y β†’ y = w
hβ‚‚
: βˆ€
y: ?m.24300
y
,
p: Ξ± β†’ Prop
p
y: ?m.24300
y
β†’
y: ?m.24300
y
=
w: Ξ±
w
) : βˆƒ!
x: ?m.24312
x
,
p: Ξ± β†’ Prop
p
x: ?m.24312
x
:= ⟨
w: Ξ±
w
,
h₁: p w
h₁
,
hβ‚‚: βˆ€ (y : Ξ±), p y β†’ y = w
hβ‚‚
⟩ theorem
ExistsUnique.elim: βˆ€ {Ξ± : Sort u} {p : Ξ± β†’ Prop} {b : Prop}, (βˆƒ! x, p x) β†’ (βˆ€ (x : Ξ±), p x β†’ (βˆ€ (y : Ξ±), p y β†’ y = x) β†’ b) β†’ b
ExistsUnique.elim
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
p: Ξ± β†’ Prop
p
:
Ξ±: Sort u
Ξ±
β†’
Prop: Type
Prop
} {
b: Prop
b
:
Prop: Type
Prop
} (
hβ‚‚: βˆƒ! x, p x
hβ‚‚
: βˆƒ!
x: ?m.24393
x
,
p: Ξ± β†’ Prop
p
x: ?m.24393
x
) (
h₁: βˆ€ (x : Ξ±), p x β†’ (βˆ€ (y : Ξ±), p y β†’ y = x) β†’ b
h₁
: βˆ€
x: ?m.24400
x
,
p: Ξ± β†’ Prop
p
x: ?m.24400
x
β†’ (βˆ€
y: ?m.24407
y
,
p: Ξ± β†’ Prop
p
y: ?m.24407
y
β†’
y: ?m.24407
y
=
x: ?m.24400
x
) β†’
b: Prop
b
) :
b: Prop
b
:=
Exists.elim: βˆ€ {Ξ± : Sort ?u.24423} {p : Ξ± β†’ Prop} {b : Prop}, (βˆƒ x, p x) β†’ (βˆ€ (a : Ξ±), p a β†’ b) β†’ b
Exists.elim
hβ‚‚: βˆƒ! x, p x
hβ‚‚
(Ξ»
w: ?m.24434
w
hw: ?m.24437
hw
=>
h₁: βˆ€ (x : Ξ±), p x β†’ (βˆ€ (y : Ξ±), p y β†’ y = x) β†’ b
h₁
w: ?m.24434
w
(
And.left: βˆ€ {a b : Prop}, a ∧ b β†’ a
And.left
hw: ?m.24437
hw
) (
And.right: βˆ€ {a b : Prop}, a ∧ b β†’ b
And.right
hw: ?m.24437
hw
)) theorem
exists_unique_of_exists_of_unique: βˆ€ {Ξ± : Sort u} {p : Ξ± β†’ Prop}, (βˆƒ x, p x) β†’ (βˆ€ (y₁ yβ‚‚ : Ξ±), p y₁ β†’ p yβ‚‚ β†’ y₁ = yβ‚‚) β†’ βˆƒ! x, p x
exists_unique_of_exists_of_unique
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
p: Ξ± β†’ Prop
p
:
Ξ±: Sort u
Ξ±
β†’
Prop: Type
Prop
} (
hex: βˆƒ x, p x
hex
: βˆƒ
x: ?m.24502
x
,
p: Ξ± β†’ Prop
p
x: ?m.24502
x
) (
hunique: βˆ€ (y₁ yβ‚‚ : Ξ±), p y₁ β†’ p yβ‚‚ β†’ y₁ = yβ‚‚
hunique
: βˆ€
y₁: ?m.24509
y₁
yβ‚‚: ?m.24512
yβ‚‚
,
p: Ξ± β†’ Prop
p
y₁: ?m.24509
y₁
β†’
p: Ξ± β†’ Prop
p
yβ‚‚: ?m.24512
yβ‚‚
β†’
y₁: ?m.24509
y₁
=
yβ‚‚: ?m.24512
yβ‚‚
) : βˆƒ!
x: ?m.24526
x
,
p: Ξ± β†’ Prop
p
x: ?m.24526
x
:=
Exists.elim: βˆ€ {Ξ± : Sort ?u.24538} {p : Ξ± β†’ Prop} {b : Prop}, (βˆƒ x, p x) β†’ (βˆ€ (a : Ξ±), p a β†’ b) β†’ b
Exists.elim
hex: βˆƒ x, p x
hex
(Ξ»
x: ?m.24552
x
px: ?m.24555
px
=>
ExistsUnique.intro: βˆ€ {Ξ± : Sort ?u.24557} {p : Ξ± β†’ Prop} (w : Ξ±), p w β†’ (βˆ€ (y : Ξ±), p y β†’ y = w) β†’ βˆƒ! x, p x
ExistsUnique.intro
x: ?m.24552
x
px: ?m.24555
px
(Ξ»
y: ?m.24566
y
(
h: p y
h
:
p: Ξ± β†’ Prop
p
y: ?m.24566
y
) =>
hunique: βˆ€ (y₁ yβ‚‚ : Ξ±), p y₁ β†’ p yβ‚‚ β†’ y₁ = yβ‚‚
hunique
y: ?m.24566
y
x: ?m.24552
x
h: p y
h
px: ?m.24555
px
)) theorem
ExistsUnique.exists: βˆ€ {Ξ± : Sort u_1} {p : Ξ± β†’ Prop}, (βˆƒ! x, p x) β†’ βˆƒ x, p x
ExistsUnique.exists
{
p: Ξ± β†’ Prop
p
:
Ξ±: ?m.24609
Ξ±
β†’
Prop: Type
Prop
} : (βˆƒ!
x: ?m.24620
x
,
p: Ξ± β†’ Prop
p
x: ?m.24620
x
) β†’ βˆƒ
x: ?m.24628
x
,
p: Ξ± β†’ Prop
p
x: ?m.24628
x
| ⟨
x: Ξ±
x
,
h: (fun x => p x) x
h
, _⟩ => ⟨
x: Ξ±
x
,
h: (fun x => p x) x
h
⟩ #align exists_of_exists_unique
ExistsUnique.exists: βˆ€ {Ξ± : Sort u_1} {p : Ξ± β†’ Prop}, (βˆƒ! x, p x) β†’ βˆƒ x, p x
ExistsUnique.exists
#align exists_unique.exists
ExistsUnique.exists: βˆ€ {Ξ± : Sort u_1} {p : Ξ± β†’ Prop}, (βˆƒ! x, p x) β†’ βˆƒ x, p x
ExistsUnique.exists
theorem
ExistsUnique.unique: βˆ€ {Ξ± : Sort u} {p : Ξ± β†’ Prop}, (βˆƒ! x, p x) β†’ βˆ€ {y₁ yβ‚‚ : Ξ±}, p y₁ β†’ p yβ‚‚ β†’ y₁ = yβ‚‚
ExistsUnique.unique
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
p: Ξ± β†’ Prop
p
:
Ξ±: Sort u
Ξ±
β†’
Prop: Type
Prop
} (
h: βˆƒ! x, p x
h
: βˆƒ!
x: ?m.24901
x
,
p: Ξ± β†’ Prop
p
x: ?m.24901
x
) {
y₁: Ξ±
y₁
yβ‚‚: Ξ±
yβ‚‚
:
Ξ±: Sort u
Ξ±
} (
py₁: p y₁
py₁
:
p: Ξ± β†’ Prop
p
y₁: Ξ±
y₁
) (
pyβ‚‚: p yβ‚‚
pyβ‚‚
:
p: Ξ± β†’ Prop
p
yβ‚‚: Ξ±
yβ‚‚
) :
y₁: Ξ±
y₁
=
yβ‚‚: Ξ±
yβ‚‚
:= let ⟨
_: Ξ±
_
, _,
hy: βˆ€ (y : Ξ±), (fun x => p x) y β†’ y = w✝
hy
⟩ :=
h: βˆƒ! x, p x
h
; (
hy: βˆ€ (y : Ξ±), (fun x => p x) y β†’ y = w✝
hy
_: Ξ±
_
py₁: p y₁
py₁
).
trans: βˆ€ {Ξ± : Sort ?u.25008} {a b c : Ξ±}, a = b β†’ b = c β†’ a = c
trans
(
hy: βˆ€ (y : Ξ±), (fun x => p x) y β†’ y = w✝
hy
_: Ξ±
_
pyβ‚‚: p yβ‚‚
pyβ‚‚
).
symm: βˆ€ {Ξ± : Sort ?u.25023} {a b : Ξ±}, a = b β†’ b = a
symm
#align unique_of_exists_unique
ExistsUnique.unique: βˆ€ {Ξ± : Sort u} {p : Ξ± β†’ Prop}, (βˆƒ! x, p x) β†’ βˆ€ {y₁ yβ‚‚ : Ξ±}, p y₁ β†’ p yβ‚‚ β†’ y₁ = yβ‚‚
ExistsUnique.unique
#align exists_unique.unique
ExistsUnique.unique: βˆ€ {Ξ± : Sort u} {p : Ξ± β†’ Prop}, (βˆƒ! x, p x) β†’ βˆ€ {y₁ yβ‚‚ : Ξ±}, p y₁ β†’ p yβ‚‚ β†’ y₁ = yβ‚‚
ExistsUnique.unique
/- exists, forall, exists unique congruences -/ -- TODO -- attribute [congr] forall_congr' -- attribute [congr] exists_congr' #align forall_congr
forall_congr': βˆ€ {Ξ± : Sort u_1} {p q : Ξ± β†’ Prop}, (βˆ€ (a : Ξ±), p a ↔ q a) β†’ ((βˆ€ (a : Ξ±), p a) ↔ βˆ€ (a : Ξ±), q a)
forall_congr'
#align Exists.imp
Exists.imp: βˆ€ {Ξ± : Sort u_1} {p q : Ξ± β†’ Prop}, (βˆ€ (a : Ξ±), p a β†’ q a) β†’ (βˆƒ a, p a) β†’ βˆƒ a, q a
Exists.imp
#align exists_imp_exists
Exists.imp: βˆ€ {Ξ± : Sort u_1} {p q : Ξ± β†’ Prop}, (βˆ€ (a : Ξ±), p a β†’ q a) β†’ (βˆƒ a, p a) β†’ βˆƒ a, q a
Exists.imp
-- @[congr] theorem
exists_unique_congr: βˆ€ {Ξ± : Sort u_1} {p q : Ξ± β†’ Prop}, (βˆ€ (a : Ξ±), p a ↔ q a) β†’ ((βˆƒ! a, p a) ↔ βˆƒ! a, q a)
exists_unique_congr
{
p: Ξ± β†’ Prop
p
q: Ξ± β†’ Prop
q
:
Ξ±: ?m.25215
Ξ±
β†’
Prop: Type
Prop
} (
h: βˆ€ (a : Ξ±), p a ↔ q a
h
: βˆ€
a: ?m.25227
a
,
p: Ξ± β†’ Prop
p
a: ?m.25227
a
↔
q: Ξ± β†’ Prop
q
a: ?m.25227
a
) : (βˆƒ!
a: ?m.25235
a
,
p: Ξ± β†’ Prop
p
a: ?m.25235
a
) ↔ βˆƒ!
a: ?m.25242
a
,
q: Ξ± β†’ Prop
q
a: ?m.25242
a
:=
exists_congr: βˆ€ {Ξ± : Sort ?u.25251} {p q : Ξ± β†’ Prop}, (βˆ€ (a : Ξ±), p a ↔ q a) β†’ ((βˆƒ a, p a) ↔ βˆƒ a, q a)
exists_congr
fun
_: ?m.25267
_
↦
and_congr: βˆ€ {a c b d : Prop}, (a ↔ c) β†’ (b ↔ d) β†’ (a ∧ b ↔ c ∧ d)
and_congr
(
h: βˆ€ (a : Ξ±), p a ↔ q a
h
_: Ξ±
_
) $
forall_congr': βˆ€ {Ξ± : Sort ?u.25284} {p q : Ξ± β†’ Prop}, (βˆ€ (a : Ξ±), p a ↔ q a) β†’ ((βˆ€ (a : Ξ±), p a) ↔ βˆ€ (a : Ξ±), q a)
forall_congr'
fun
_: ?m.25297
_
↦
imp_congr_left: βˆ€ {a b c : Prop}, (a ↔ b) β†’ (a β†’ c ↔ b β†’ c)
imp_congr_left
(
h: βˆ€ (a : Ξ±), p a ↔ q a
h
_: Ξ±
_
) /- decidable -/ #align decidable.to_bool
Decidable.decide: (p : Prop) β†’ [h : Decidable p] β†’ Bool
Decidable.decide
theorem
decide_True': βˆ€ (h : Decidable True), decide True = true
decide_True'
(h :
Decidable: Prop β†’ Type
Decidable
True: Prop
True
) :
decide: (p : Prop) β†’ [h : Decidable p] β†’ Bool
decide
True: Prop
True
=
true: Bool
true
:=

Goals accomplished! πŸ™
a, b, c, d: Prop

p: ?m.25343

h: Decidable True



Goals accomplished! πŸ™
#align to_bool_true_eq_tt
decide_True': βˆ€ (h : Decidable True), decide True = true
decide_True'
theorem
decide_False': βˆ€ (h : Decidable False), decide False = false
decide_False'
(h :
Decidable: Prop β†’ Type
Decidable
False: Prop
False
) :
decide: (p : Prop) β†’ [h : Decidable p] β†’ Bool
decide
False: Prop
False
=
false: Bool
false
:=

Goals accomplished! πŸ™
a, b, c, d: Prop

p: ?m.25417

h: Decidable False



Goals accomplished! πŸ™
#align to_bool_false_eq_ff
decide_False': βˆ€ (h : Decidable False), decide False = false
decide_False'
namespace Decidable def
recOn_true: [h : Decidable p] β†’ {h₁ : p β†’ Sort u} β†’ {hβ‚‚ : Β¬p β†’ Sort u} β†’ (h₃ : p) β†’ h₁ h₃ β†’ Decidable.recOn h hβ‚‚ h₁
recOn_true
[h :
Decidable: Prop β†’ Type
Decidable
p: ?m.25511
p
] {
h₁: p β†’ Sort u
h₁
:
p: ?m.25511
p
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} {
hβ‚‚: Β¬p β†’ Sort u
hβ‚‚
: Β¬
p: ?m.25511
p
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} (
h₃: p
h₃
:
p: ?m.25511
p
) (
hβ‚„: h₁ h₃
hβ‚„
:
h₁: p β†’ Sort u
h₁
h₃: p
h₃
) :
Decidable.recOn: {p : Prop} β†’ {motive : Decidable p β†’ Sort ?u.25528} β†’ (t : Decidable p) β†’ ((h : Β¬p) β†’ motive (isFalse h)) β†’ ((h : p) β†’ motive (isTrue h)) β†’ motive t
Decidable.recOn
h
hβ‚‚: Β¬p β†’ Sort u
hβ‚‚
h₁: p β†’ Sort u
h₁
:=
cast: {Ξ± Ξ² : Sort ?u.25569} β†’ Ξ± = Ξ² β†’ Ξ± β†’ Ξ²
cast
(

Goals accomplished! πŸ™
a, b, c, d, p: Prop

h: Decidable p

h₁: p β†’ Sort u

hβ‚‚: Β¬p β†’ Sort u

h₃: p

hβ‚„: h₁ h₃


h₁ h₃ = Decidable.recOn h hβ‚‚ h₁
a, b, c, d, p: Prop

h: Decidable p

h₁: p β†’ Sort u

hβ‚‚: Β¬p β†’ Sort u

h₃: p

hβ‚„: h₁ h₃


h₁ h₃ = Decidable.recOn h hβ‚‚ h₁
a, b, c, d, p: Prop

h: Decidable p

h₁: p β†’ Sort u

hβ‚‚: Β¬p β†’ Sort u

h₃: p

hβ‚„: h₁ h₃

h✝: p


h₁ h₃ = Decidable.recOn (isTrue h✝) hβ‚‚ h₁
a, b, c, d, p: Prop

h: Decidable p

h₁: p β†’ Sort u

hβ‚‚: Β¬p β†’ Sort u

h₃: p

hβ‚„: h₁ h₃


h₁ h₃ = Decidable.recOn h hβ‚‚ h₁

Goals accomplished! πŸ™
)
hβ‚„: h₁ h₃
hβ‚„
#align decidable.rec_on_true
Decidable.recOn_true: (p : Prop) β†’ [h : Decidable p] β†’ {h₁ : p β†’ Sort u} β†’ {hβ‚‚ : Β¬p β†’ Sort u} β†’ (h₃ : p) β†’ h₁ h₃ β†’ Decidable.recOn h hβ‚‚ h₁
Decidable.recOn_true
def
recOn_false: [h : Decidable p] β†’ {h₁ : p β†’ Sort u} β†’ {hβ‚‚ : Β¬p β†’ Sort u} β†’ (h₃ : Β¬p) β†’ hβ‚‚ h₃ β†’ Decidable.recOn h hβ‚‚ h₁
recOn_false
[h :
Decidable: Prop β†’ Type
Decidable
p: ?m.25773
p
] {
h₁: p β†’ Sort u
h₁
:
p: ?m.25773
p
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} {
hβ‚‚: Β¬p β†’ Sort u
hβ‚‚
: Β¬
p: ?m.25773
p
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} (
h₃: Β¬p
h₃
: Β¬
p: ?m.25773
p
) (
hβ‚„: hβ‚‚ h₃
hβ‚„
:
hβ‚‚: Β¬p β†’ Sort u
hβ‚‚
h₃: Β¬p
h₃
) :
Decidable.recOn: {p : Prop} β†’ {motive : Decidable p β†’ Sort ?u.25791} β†’ (t : Decidable p) β†’ ((h : Β¬p) β†’ motive (isFalse h)) β†’ ((h : p) β†’ motive (isTrue h)) β†’ motive t
Decidable.recOn
h
hβ‚‚: Β¬p β†’ Sort u
hβ‚‚
h₁: p β†’ Sort u
h₁
:=
cast: {Ξ± Ξ² : Sort ?u.25832} β†’ Ξ± = Ξ² β†’ Ξ± β†’ Ξ²
cast
(

Goals accomplished! πŸ™
a, b, c, d, p: Prop

h: Decidable p

h₁: p β†’ Sort u

hβ‚‚: Β¬p β†’ Sort u

h₃: Β¬p

hβ‚„: hβ‚‚ h₃


hβ‚‚ h₃ = Decidable.recOn h hβ‚‚ h₁
a, b, c, d, p: Prop

h: Decidable p

h₁: p β†’ Sort u

hβ‚‚: Β¬p β†’ Sort u

h₃: Β¬p

hβ‚„: hβ‚‚ h₃


hβ‚‚ h₃ = Decidable.recOn h hβ‚‚ h₁
a, b, c, d, p: Prop

h: Decidable p

h₁: p β†’ Sort u

hβ‚‚: Β¬p β†’ Sort u

h₃: Β¬p

hβ‚„: hβ‚‚ h₃

h✝: ¬p


hβ‚‚ h₃ = Decidable.recOn (isFalse h✝) hβ‚‚ h₁
a, b, c, d, p: Prop

h: Decidable p

h₁: p β†’ Sort u

hβ‚‚: Β¬p β†’ Sort u

h₃: Β¬p

hβ‚„: hβ‚‚ h₃


hβ‚‚ h₃ = Decidable.recOn h hβ‚‚ h₁

Goals accomplished! πŸ™
)
hβ‚„: hβ‚‚ h₃
hβ‚„
#align decidable.rec_on_false
Decidable.recOn_false: (p : Prop) β†’ [h : Decidable p] β†’ {h₁ : p β†’ Sort u} β†’ {hβ‚‚ : Β¬p β†’ Sort u} β†’ (h₃ : Β¬p) β†’ hβ‚‚ h₃ β†’ Decidable.recOn h hβ‚‚ h₁
Decidable.recOn_false
alias
byCases: {p : Prop} β†’ {q : Sort u} β†’ [dec : Decidable p] β†’ (p β†’ q) β†’ (Β¬p β†’ q) β†’ q
byCases
←
by_cases: {p : Prop} β†’ {q : Sort u} β†’ [dec : Decidable p] β†’ (p β†’ q) β†’ (Β¬p β†’ q) β†’ q
by_cases
alias
byContradiction: βˆ€ {p : Prop} [dec : Decidable p], (Β¬p β†’ False) β†’ p
byContradiction
←
by_contradiction: βˆ€ {p : Prop} [dec : Decidable p], (Β¬p β†’ False) β†’ p
by_contradiction
alias
not_not: βˆ€ {p : Prop} [inst : Decidable p], ¬¬p ↔ p
not_not
←
not_not_iff: βˆ€ {p : Prop} [inst : Decidable p], ¬¬p ↔ p
not_not_iff
@[deprecated
not_or: βˆ€ {p q : Prop}, Β¬(p ∨ q) ↔ Β¬p ∧ Β¬q
not_or
] theorem
not_or_iff_and_not: βˆ€ (p q : Prop) [inst : Decidable p] [inst : Decidable q], Β¬(p ∨ q) ↔ Β¬p ∧ Β¬q
not_or_iff_and_not
(
p: Prop
p
q: ?m.26150
q
) [
Decidable: Prop β†’ Type
Decidable
p: ?m.26147
p
] [
Decidable: Prop β†’ Type
Decidable
q: ?m.26150
q
] : Β¬(
p: ?m.26147
p
∨
q: ?m.26150
q
) ↔ Β¬
p: ?m.26147
p
∧ ¬
q: ?m.26150
q
:=
not_or: βˆ€ {p q : Prop}, Β¬(p ∨ q) ↔ Β¬p ∧ Β¬q
not_or
end Decidable #align decidable_of_decidable_of_iff
decidable_of_decidable_of_iff: {p q : Prop} β†’ [inst : Decidable p] β†’ (p ↔ q) β†’ Decidable q
decidable_of_decidable_of_iff
#align decidable_of_decidable_of_eq
decidable_of_decidable_of_eq: {p q : Prop} β†’ [inst : Decidable p] β†’ p = q β†’ Decidable q
decidable_of_decidable_of_eq
#align or.by_cases
Or.by_cases: {p q : Prop} β†’ [inst : Decidable p] β†’ {Ξ± : Sort u} β†’ p ∨ q β†’ (p β†’ Ξ±) β†’ (q β†’ Ξ±) β†’ Ξ±
Or.by_cases
alias
instDecidableOr: {p q : Prop} β†’ [dp : Decidable p] β†’ [dq : Decidable q] β†’ Decidable (p ∨ q)
instDecidableOr
←
Or.decidable: {p q : Prop} β†’ [dp : Decidable p] β†’ [dq : Decidable q] β†’ Decidable (p ∨ q)
Or.decidable
alias
instDecidableAnd: {p q : Prop} β†’ [dp : Decidable p] β†’ [dq : Decidable q] β†’ Decidable (p ∧ q)
instDecidableAnd
←
And.decidable: {p q : Prop} β†’ [dp : Decidable p] β†’ [dq : Decidable q] β†’ Decidable (p ∧ q)
And.decidable
alias
instDecidableNot: {p : Prop} β†’ [dp : Decidable p] β†’ Decidable Β¬p
instDecidableNot
←
Not.decidable: {p : Prop} β†’ [dp : Decidable p] β†’ Decidable Β¬p
Not.decidable
alias
instDecidableIff: {p q : Prop} β†’ [inst : Decidable p] β†’ [inst : Decidable q] β†’ Decidable (p ↔ q)
instDecidableIff
←
Iff.decidable: {p q : Prop} β†’ [inst : Decidable p] β†’ [inst : Decidable q] β†’ Decidable (p ↔ q)
Iff.decidable
alias
instDecidableTrue: Decidable True
instDecidableTrue
←
decidableTrue: Decidable True
decidableTrue
alias
instDecidableFalse: Decidable False
instDecidableFalse
←
decidableFalse: Decidable False
decidableFalse
#align decidable.true
decidableTrue: Decidable True
decidableTrue
#align decidable.false
decidableFalse: Decidable False
decidableFalse
#align or.decidable
Or.decidable: {p q : Prop} β†’ [dp : Decidable p] β†’ [dq : Decidable q] β†’ Decidable (p ∨ q)
Or.decidable
#align and.decidable
And.decidable: {p q : Prop} β†’ [dp : Decidable p] β†’ [dq : Decidable q] β†’ Decidable (p ∧ q)
And.decidable
#align not.decidable
Not.decidable: {p : Prop} β†’ [dp : Decidable p] β†’ Decidable Β¬p
Not.decidable
#align iff.decidable
Iff.decidable: {p q : Prop} β†’ [inst : Decidable p] β†’ [inst : Decidable q] β†’ Decidable (p ↔ q)
Iff.decidable
instance: (p : Prop) β†’ {q : Prop} β†’ [inst : Decidable p] β†’ [inst : Decidable q] β†’ Decidable (Xor' p q)
instance
[
Decidable: Prop β†’ Type
Decidable
p: ?m.26454
p
] [
Decidable: Prop β†’ Type
Decidable
q: ?m.26460
q
] :
Decidable: Prop β†’ Type
Decidable
(
Xor': Prop β†’ Prop β†’ Prop
Xor'
p: ?m.26454
p
q: ?m.26460
q
) :=
inferInstanceAs: (Ξ± : Sort ?u.26471) β†’ [i : Ξ±] β†’ Ξ±
inferInstanceAs
(
Decidable: Prop β†’ Type
Decidable
(
Or: Prop β†’ Prop β†’ Prop
Or
..)) def
IsDecEq: {Ξ± : Sort u} β†’ (Ξ± β†’ Ξ± β†’ Bool) β†’ Prop
IsDecEq
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} (
p: Ξ± β†’ Ξ± β†’ Bool
p
:
Ξ±: Sort u
Ξ±
β†’
Ξ±: Sort u
Ξ±
β†’
Bool: Type
Bool
) :
Prop: Type
Prop
:= βˆ€ ⦃
x: Ξ±
x
y: Ξ±
y
:
Ξ±: Sort u
Ξ±
⦄,
p: Ξ± β†’ Ξ± β†’ Bool
p
x: Ξ±
x
y: Ξ±
y
=
true: Bool
true
β†’
x: Ξ±
x
=
y: Ξ±
y
def
IsDecRefl: {Ξ± : Sort u} β†’ (Ξ± β†’ Ξ± β†’ Bool) β†’ Prop
IsDecRefl
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} (
p: Ξ± β†’ Ξ± β†’ Bool
p
:
Ξ±: Sort u
Ξ±
β†’
Ξ±: Sort u
Ξ±
β†’
Bool: Type
Bool
) :
Prop: Type
Prop
:= βˆ€
x: ?m.26967
x
,
p: Ξ± β†’ Ξ± β†’ Bool
p
x: ?m.26967
x
x: ?m.26967
x
=
true: Bool
true
def
decidableEq_of_bool_pred: {Ξ± : Sort u} β†’ {p : Ξ± β†’ Ξ± β†’ Bool} β†’ IsDecEq p β†’ IsDecRefl p β†’ DecidableEq Ξ±
decidableEq_of_bool_pred
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
p: Ξ± β†’ Ξ± β†’ Bool
p
:
Ξ±: Sort u
Ξ±
β†’
Ξ±: Sort u
Ξ±
β†’
Bool: Type
Bool
} (
h₁: IsDecEq p
h₁
:
IsDecEq: {Ξ± : Sort ?u.27003} β†’ (Ξ± β†’ Ξ± β†’ Bool) β†’ Prop
IsDecEq
p: Ξ± β†’ Ξ± β†’ Bool
p
) (
hβ‚‚: IsDecRefl p
hβ‚‚
:
IsDecRefl: {Ξ± : Sort ?u.27013} β†’ (Ξ± β†’ Ξ± β†’ Bool) β†’ Prop
IsDecRefl
p: Ξ± β†’ Ξ± β†’ Bool
p
) :
DecidableEq: Sort ?u.27023 β†’ Sort (max1?u.27023)
DecidableEq
Ξ±: Sort u
Ξ±
|
x: Ξ±
x
,
y: Ξ±
y
=> if
hp: ?m.27088
hp
:
p: Ξ± β†’ Ξ± β†’ Bool
p
x: Ξ±
x
y: Ξ±
y
=
true: Bool
true
then
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
(
h₁: IsDecEq p
h₁
hp: ?m.27074
hp
) else
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
(Ξ»
hxy: x = y
hxy
:
x: Ξ±
x
=
y: Ξ±
y
=>
absurd: βˆ€ {a : Prop} {b : Sort ?u.27095}, a β†’ Β¬a β†’ b
absurd
(
hβ‚‚: IsDecRefl p
hβ‚‚
y: Ξ±
y
) (

Goals accomplished! πŸ™
a, b, c, d: Prop

p✝: ?m.26992

Ξ±: Sort u

p: Ξ± β†’ Ξ± β†’ Bool

h₁: IsDecEq p

hβ‚‚: IsDecRefl p

x, y: Ξ±

hp: Β¬p x y = true

hxy: x = y


Β¬p y y = true
a, b, c, d: Prop

p✝: ?m.26992

Ξ±: Sort u

p: Ξ± β†’ Ξ± β†’ Bool

h₁: IsDecEq p

hβ‚‚: IsDecRefl p

x, y: Ξ±

hp: Β¬p x y = true

hxy: x = y


Β¬p y y = true
a, b, c, d: Prop

p✝: ?m.26992

Ξ±: Sort u

p: Ξ± β†’ Ξ± β†’ Bool

h₁: IsDecEq p

hβ‚‚: IsDecRefl p

x, y: Ξ±

hp: Β¬p y y = true

hxy: x = y


Β¬p y y = true
a, b, c, d: Prop

p✝: ?m.26992

Ξ±: Sort u

p: Ξ± β†’ Ξ± β†’ Bool

h₁: IsDecEq p

hβ‚‚: IsDecRefl p

x, y: Ξ±

hp: Β¬p y y = true

hxy: x = y


Β¬p y y = true

Goals accomplished! πŸ™
)) #align decidable_eq_of_bool_pred
decidableEq_of_bool_pred: {Ξ± : Sort u} β†’ {p : Ξ± β†’ Ξ± β†’ Bool} β†’ IsDecEq p β†’ IsDecRefl p β†’ DecidableEq Ξ±
decidableEq_of_bool_pred
theorem
decidableEq_inl_refl: βˆ€ {Ξ± : Sort u} [h : DecidableEq Ξ±] (a : Ξ±), h a a = isTrue (_ : a = a)
decidableEq_inl_refl
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} [
h: DecidableEq Ξ±
h
:
DecidableEq: Sort ?u.27347 β†’ Sort (max1?u.27347)
DecidableEq
Ξ±: Sort u
Ξ±
] (
a: Ξ±
a
:
Ξ±: Sort u
Ξ±
) :
h: DecidableEq Ξ±
h
a: Ξ±
a
a: Ξ±
a
=
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
(
Eq.refl: βˆ€ {Ξ± : Sort ?u.27360} (a : Ξ±), a = a
Eq.refl
a: Ξ±
a
) := match
h: DecidableEq Ξ±
h
a: Ξ±
a
a: Ξ±
a
with |
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
_ =>
rfl: βˆ€ {Ξ± : Sort ?u.27387} {a : Ξ±}, a = a
rfl
theorem
decidableEq_inr_neg: βˆ€ {Ξ± : Sort u} [h : DecidableEq Ξ±] {a b : Ξ±} (n : a β‰  b), h a b = isFalse n
decidableEq_inr_neg
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} [
h: DecidableEq Ξ±
h
:
DecidableEq: Sort ?u.27472 β†’ Sort (max1?u.27472)
DecidableEq
Ξ±: Sort u
Ξ±
] {
a: Ξ±
a
b: Ξ±
b
:
Ξ±: Sort u
Ξ±
} (
n: a β‰  b
n
:
a: Ξ±
a
β‰ 
b: Ξ±
b
) :
h: DecidableEq Ξ±
h
a: Ξ±
a
b: Ξ±
b
=
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
n: a β‰  b
n
:= match
h: DecidableEq Ξ±
h
a: Ξ±
a
b: Ξ±
b
with |
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
_ =>
rfl: βˆ€ {Ξ± : Sort ?u.27517} {a : Ξ±}, a = a
rfl
#align inhabited.default
Inhabited.default: {Ξ± : Sort u} β†’ [self : Inhabited Ξ±] β†’ Ξ±
Inhabited.default
#align arbitrary
Inhabited.default: {Ξ± : Sort u} β†’ [self : Inhabited Ξ±] β†’ Ξ±
Inhabited.default
#align nonempty_of_inhabited
instNonempty: βˆ€ {Ξ± : Sort u} [inst : Inhabited Ξ±], Nonempty Ξ±
instNonempty
/- subsingleton -/ theorem
rec_subsingleton: βˆ€ {p : Prop} [h : Decidable p] {h₁ : p β†’ Sort u} {hβ‚‚ : Β¬p β†’ Sort u} [h₃ : βˆ€ (h : p), Subsingleton (h₁ h)] [hβ‚„ : βˆ€ (h : Β¬p), Subsingleton (hβ‚‚ h)], Subsingleton (Decidable.recOn h hβ‚‚ h₁)
rec_subsingleton
{
p: Prop
p
:
Prop: Type
Prop
} [h :
Decidable: Prop β†’ Type
Decidable
p: Prop
p
] {
h₁: p β†’ Sort u
h₁
:
p: Prop
p
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} {
hβ‚‚: Β¬p β†’ Sort u
hβ‚‚
: Β¬
p: Prop
p
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} [
h₃: βˆ€ (h : p), Subsingleton (h₁ h)
h₃
: βˆ€
h: p
h
:
p: Prop
p
,
Subsingleton: Sort ?u.27734 β†’ Prop
Subsingleton
(
h₁: p β†’ Sort u
h₁
h: p
h
)] [
hβ‚„: βˆ€ (h : Β¬p), Subsingleton (hβ‚‚ h)
hβ‚„
: βˆ€
h: Β¬p
h
: Β¬
p: Prop
p
,
Subsingleton: Sort ?u.27741 β†’ Prop
Subsingleton
(
hβ‚‚: Β¬p β†’ Sort u
hβ‚‚
h: Β¬p
h
)] :
Subsingleton: Sort ?u.27746 β†’ Prop
Subsingleton
(
Decidable.recOn: {p : Prop} β†’ {motive : Decidable p β†’ Sort ?u.27747} β†’ (t : Decidable p) β†’ ((h : Β¬p) β†’ motive (isFalse h)) β†’ ((h : p) β†’ motive (isTrue h)) β†’ motive t
Decidable.recOn
h
hβ‚‚: Β¬p β†’ Sort u
hβ‚‚
h₁: p β†’ Sort u
h₁
) := match h with |
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
h: p
h
=>
h₃: βˆ€ (h : p), Subsingleton (h₁ h)
h₃
h: p
h
|
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
h: Β¬p
h
=>
hβ‚„: βˆ€ (h : Β¬p), Subsingleton (hβ‚‚ h)
hβ‚„
h: Β¬p
h
@[deprecated
ite_self: βˆ€ {Ξ± : Sort u} {c : Prop} {d : Decidable c} (a : Ξ±), (if c then a else a) = a
ite_self
] theorem
if_t_t: βˆ€ (c : Prop) [inst : Decidable c] {Ξ± : Sort u} (t : Ξ±), (if c then t else t) = t
if_t_t
(
c: Prop
c
:
Prop: Type
Prop
) [
Decidable: Prop β†’ Type
Decidable
c: Prop
c
] {
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} (
t: Ξ±
t
:
Ξ±: Sort u
Ξ±
) :
ite: {Ξ± : Sort ?u.27913} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
c: Prop
c
t: Ξ±
t
t: Ξ±
t
=
t: Ξ±
t
:=
ite_self: βˆ€ {Ξ± : Sort ?u.27923} {c : Prop} {d : Decidable c} (a : Ξ±), (if c then a else a) = a
ite_self
_: ?m.27924
_
theorem
imp_of_if_pos: βˆ€ {c t e : Prop} [inst : Decidable c], (if c then t else e) β†’ c β†’ t
imp_of_if_pos
{
c: Prop
c
t: Prop
t
e: Prop
e
:
Prop: Type
Prop
} [
Decidable: Prop β†’ Type
Decidable
c: Prop
c
] (
h: if c then t else e
h
:
ite: {Ξ± : Sort ?u.27961} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
c: Prop
c
t: Prop
t
e: Prop
e
) (
hc: c
hc
:
c: Prop
c
) :
t: Prop
t
:=

Goals accomplished! πŸ™
a, b, c✝, d: Prop

p: ?m.27950

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hc: c


t
a, b, c✝, d: Prop

p: ?m.27950

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hc: c

this: t


t
a, b, c✝, d: Prop

p: ?m.27950

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hc: c

this: t


t
a, b, c✝, d: Prop

p: ?m.27950

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hc: c


t

Goals accomplished! πŸ™
#align implies_of_if_pos
imp_of_if_pos: βˆ€ {c t e : Prop} [inst : Decidable c], (if c then t else e) β†’ c β†’ t
imp_of_if_pos
theorem
imp_of_if_neg: βˆ€ {c t e : Prop} [inst : Decidable c], (if c then t else e) β†’ Β¬c β†’ e
imp_of_if_neg
{
c: Prop
c
t: Prop
t
e: Prop
e
:
Prop: Type
Prop
} [
Decidable: Prop β†’ Type
Decidable
c: Prop
c
] (
h: if c then t else e
h
:
ite: {Ξ± : Sort ?u.28032} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
c: Prop
c
t: Prop
t
e: Prop
e
) (
hnc: Β¬c
hnc
: Β¬
c: Prop
c
) :
e: Prop
e
:=

Goals accomplished! πŸ™
a, b, c✝, d: Prop

p: ?m.28021

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hnc: Β¬c


e
a, b, c✝, d: Prop

p: ?m.28021

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hnc: Β¬c

this: e


e
a, b, c✝, d: Prop

p: ?m.28021

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hnc: Β¬c

this: e


e
a, b, c✝, d: Prop

p: ?m.28021

c, t, e: Prop

inst✝: Decidable c

h: if c then t else e

hnc: Β¬c


e

Goals accomplished! πŸ™
#align implies_of_if_neg
imp_of_if_neg: βˆ€ {c t e : Prop} [inst : Decidable c], (if c then t else e) β†’ Β¬c β†’ e
imp_of_if_neg
theorem
if_ctx_congr: βˆ€ {Ξ± : Sort u} {b c : Prop} [dec_b : Decidable b] [dec_c : Decidable c] {x y u v : Ξ±}, (b ↔ c) β†’ (c β†’ x = u) β†’ (Β¬c β†’ y = v) β†’ (if b then x else y) = if c then u else v
if_ctx_congr
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
b: Prop
b
c: Prop
c
:
Prop: Type
Prop
} [
dec_b: Decidable b
dec_b
:
Decidable: Prop β†’ Type
Decidable
b: Prop
b
] [
dec_c: Decidable c
dec_c
:
Decidable: Prop β†’ Type
Decidable
c: Prop
c
] {
x: Ξ±
x
y: Ξ±
y
u: Ξ±
u
v: Ξ±
v
:
Ξ±: Sort u
Ξ±
} (
h_c: b ↔ c
h_c
:
b: Prop
b
↔
c: Prop
c
) (
h_t: c β†’ x = u
h_t
:
c: Prop
c
β†’
x: Ξ±
x
=
u: Ξ±
u
) (
h_e: Β¬c β†’ y = v
h_e
: Β¬
c: Prop
c
β†’
y: Ξ±
y
=
v: Ξ±
v
) :
ite: {Ξ± : Sort ?u.28130} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
b: Prop
b
x: Ξ±
x
y: Ξ±
y
=
ite: {Ξ± : Sort ?u.28135} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
c: Prop
c
u: Ξ±
u
v: Ξ±
v
:= match
dec_b: Decidable b
dec_b
,
dec_c: Decidable c
dec_c
with |
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
_,
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
hβ‚‚: Β¬c
hβ‚‚
=>
h_e: Β¬c β†’ y = v
h_e
hβ‚‚: Β¬c
hβ‚‚
|
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
_,
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
hβ‚‚: c
hβ‚‚
=>
h_t: c β†’ x = u
h_t
hβ‚‚: c
hβ‚‚
|
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
h₁: Β¬b
h₁
,
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
hβ‚‚: c
hβ‚‚
=>
absurd: βˆ€ {a : Prop} {b : Sort ?u.28232}, a β†’ Β¬a β†’ b
absurd
hβ‚‚: c
hβ‚‚
(
Iff.mp: βˆ€ {a b : Prop}, (a ↔ b) β†’ a β†’ b
Iff.mp
(
not_congr: βˆ€ {a b : Prop}, (a ↔ b) β†’ (Β¬a ↔ Β¬b)
not_congr
h_c: b ↔ c
h_c
)
h₁: Β¬b
h₁
) |
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
h₁: b
h₁
,
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
hβ‚‚: Β¬c
hβ‚‚
=>
absurd: βˆ€ {a : Prop} {b : Sort ?u.28267}, a β†’ Β¬a β†’ b
absurd
h₁: b
h₁
(
Iff.mpr: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
Iff.mpr
(
not_congr: βˆ€ {a b : Prop}, (a ↔ b) β†’ (Β¬a ↔ Β¬b)
not_congr
h_c: b ↔ c
h_c
)
hβ‚‚: Β¬c
hβ‚‚
) theorem
if_congr: βˆ€ {Ξ± : Sort u} {b c : Prop} [inst : Decidable b] [inst_1 : Decidable c] {x y u v : Ξ±}, (b ↔ c) β†’ x = u β†’ y = v β†’ (if b then x else y) = if c then u else v
if_congr
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
b: Prop
b
c: Prop
c
:
Prop: Type
Prop
} [
Decidable: Prop β†’ Type
Decidable
b: Prop
b
] [
Decidable: Prop β†’ Type
Decidable
c: Prop
c
] {
x: Ξ±
x
y: Ξ±
y
u: Ξ±
u
v: Ξ±
v
:
Ξ±: Sort u
Ξ±
} (
h_c: b ↔ c
h_c
:
b: Prop
b
↔
c: Prop
c
) (
h_t: x = u
h_t
:
x: Ξ±
x
=
u: Ξ±
u
) (
h_e: y = v
h_e
:
y: Ξ±
y
=
v: Ξ±
v
) :
ite: {Ξ± : Sort ?u.28509} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
b: Prop
b
x: Ξ±
x
y: Ξ±
y
=
ite: {Ξ± : Sort ?u.28514} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
c: Prop
c
u: Ξ±
u
v: Ξ±
v
:=
if_ctx_congr: βˆ€ {Ξ± : Sort ?u.28532} {b c : Prop} [dec_b : Decidable b] [dec_c : Decidable c] {x y u v : Ξ±}, (b ↔ c) β†’ (c β†’ x = u) β†’ (Β¬c β†’ y = v) β†’ (if b then x else y) = if c then u else v
if_ctx_congr
h_c: b ↔ c
h_c
(Ξ»
_: ?m.28618
_
=>
h_t: x = u
h_t
) (Ξ»
_: ?m.28623
_
=>
h_e: y = v
h_e
) theorem
if_ctx_congr_prop: βˆ€ {b c x y u v : Prop} [dec_b : Decidable b] [dec_c : Decidable c], (b ↔ c) β†’ (c β†’ (x ↔ u)) β†’ (Β¬c β†’ (y ↔ v)) β†’ ((if b then x else y) ↔ if c then u else v)
if_ctx_congr_prop
{
b: Prop
b
c: Prop
c
x: Prop
x
y: Prop
y
u: Prop
u
v: Prop
v
:
Prop: Type
Prop
} [
dec_b: Decidable b
dec_b
:
Decidable: Prop β†’ Type
Decidable
b: Prop
b
] [
dec_c: Decidable c
dec_c
:
Decidable: Prop β†’ Type
Decidable
c: Prop
c
] (
h_c: b ↔ c
h_c
:
b: Prop
b
↔
c: Prop
c
) (
h_t: c β†’ (x ↔ u)
h_t
:
c: Prop
c
β†’ (
x: Prop
x
↔
u: Prop
u
)) (
h_e: Β¬c β†’ (y ↔ v)
h_e
: Β¬
c: Prop
c
β†’ (
y: Prop
y
↔
v: Prop
v
)) :
ite: {Ξ± : Sort ?u.28682} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
b: Prop
b
x: Prop
x
y: Prop
y
↔
ite: {Ξ± : Sort ?u.28687} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
c: Prop
c
u: Prop
u
v: Prop
v
:= match
dec_b: Decidable b
dec_b
,
dec_c: Decidable c
dec_c
with |
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
_,
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
hβ‚‚: Β¬c
hβ‚‚
=>
h_e: Β¬c β†’ (y ↔ v)
h_e
hβ‚‚: Β¬c
hβ‚‚
|
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
_,
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
hβ‚‚: c
hβ‚‚
=>
h_t: c β†’ (x ↔ u)
h_t
hβ‚‚: c
hβ‚‚
|
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
h₁: Β¬b
h₁
,
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
hβ‚‚: c
hβ‚‚
=>
absurd: βˆ€ {a : Prop} {b : Sort ?u.28781}, a β†’ Β¬a β†’ b
absurd
hβ‚‚: c
hβ‚‚
(
Iff.mp: βˆ€ {a b : Prop}, (a ↔ b) β†’ a β†’ b
Iff.mp
(
not_congr: βˆ€ {a b : Prop}, (a ↔ b) β†’ (Β¬a ↔ Β¬b)
not_congr
h_c: b ↔ c
h_c
)
h₁: Β¬b
h₁
) |
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
h₁: b
h₁
,
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
hβ‚‚: Β¬c
hβ‚‚
=>
absurd: βˆ€ {a : Prop} {b : Sort ?u.28814}, a β†’ Β¬a β†’ b
absurd
h₁: b
h₁
(
Iff.mpr: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
Iff.mpr
(
not_congr: βˆ€ {a b : Prop}, (a ↔ b) β†’ (Β¬a ↔ Β¬b)
not_congr
h_c: b ↔ c
h_c
)
hβ‚‚: Β¬c
hβ‚‚
) -- @[congr] theorem
if_congr_prop: βˆ€ {b c x y u v : Prop} [inst : Decidable b] [inst_1 : Decidable c], (b ↔ c) β†’ (x ↔ u) β†’ (y ↔ v) β†’ ((if b then x else y) ↔ if c then u else v)
if_congr_prop
{
b: Prop
b
c: Prop
c
x: Prop
x
y: Prop
y
u: Prop
u
v: Prop
v
:
Prop: Type
Prop
} [
Decidable: Prop β†’ Type
Decidable
b: Prop
b
] [
Decidable: Prop β†’ Type
Decidable
c: Prop
c
] (
h_c: b ↔ c
h_c
:
b: Prop
b
↔
c: Prop
c
) (
h_t: x ↔ u
h_t
:
x: Prop
x
↔
u: Prop
u
) (
h_e: y ↔ v
h_e
:
y: Prop
y
↔
v: Prop
v
) :
ite: {Ξ± : Sort ?u.29029} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
b: Prop
b
x: Prop
x
y: Prop
y
↔
ite: {Ξ± : Sort ?u.29034} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
c: Prop
c
u: Prop
u
v: Prop
v
:=
if_ctx_congr_prop: βˆ€ {b c x y u v : Prop} [dec_b : Decidable b] [dec_c : Decidable c], (b ↔ c) β†’ (c β†’ (x ↔ u)) β†’ (Β¬c β†’ (y ↔ v)) β†’ ((if b then x else y) ↔ if c then u else v)
if_ctx_congr_prop
h_c: b ↔ c
h_c
(Ξ»
_: ?m.29131
_
=>
h_t: x ↔ u
h_t
) (Ξ»
_: ?m.29136
_
=>
h_e: y ↔ v
h_e
) theorem
if_ctx_simp_congr_prop: βˆ€ {b c x y u v : Prop} [inst : Decidable b] (h_c : b ↔ c), (c β†’ (x ↔ u)) β†’ (Β¬c β†’ (y ↔ v)) β†’ ((if b then x else y) ↔ if c then u else v)
if_ctx_simp_congr_prop
{
b: Prop
b
c: Prop
c
x: Prop
x
y: Prop
y
u: Prop
u
v: Prop
v
:
Prop: Type
Prop
} [
Decidable: Prop β†’ Type
Decidable
b: Prop
b
] (
h_c: b ↔ c
h_c
:
b: Prop
b
↔
c: Prop
c
) (
h_t: c β†’ (x ↔ u)
h_t
:
c: Prop
c
β†’ (
x: Prop
x
↔
u: Prop
u
)) -- FIXME: after https://github.com/leanprover/lean4/issues/1867 is fixed, -- this should be changed back to: -- (h_e : Β¬c β†’ (y ↔ v)) : ite b x y ↔ ite c (h := decidable_of_decidable_of_iff h_c) u v := (
h_e: Β¬c β†’ (y ↔ v)
h_e
: Β¬
c: Prop
c
β†’ (
y: Prop
y
↔
v: Prop
v
)) :
ite: {Ξ± : Sort ?u.29192} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
b: Prop
b
x: Prop
x
y: Prop
y
↔ @
ite: {Ξ± : Sort ?u.29196} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
_: Sort ?u.29196
_
c: Prop
c
(
decidable_of_decidable_of_iff: {p q : Prop} β†’ [inst : Decidable p] β†’ (p ↔ q) β†’ Decidable q
decidable_of_decidable_of_iff
h_c: b ↔ c
h_c
)
u: Prop
u
v: Prop
v
:=
if_ctx_congr_prop: βˆ€ {b c x y u v : Prop} [dec_b : Decidable b] [dec_c : Decidable c], (b ↔ c) β†’ (c β†’ (x ↔ u)) β†’ (Β¬c β†’ (y ↔ v)) β†’ ((if b then x else y) ↔ if c then u else v)
if_ctx_congr_prop
(dec_c :=
decidable_of_decidable_of_iff: {p q : Prop} β†’ [inst : Decidable p] β†’ (p ↔ q) β†’ Decidable q
decidable_of_decidable_of_iff
h_c: b ↔ c
h_c
)
h_c: b ↔ c
h_c
h_t: c β†’ (x ↔ u)
h_t
h_e: Β¬c β†’ (y ↔ v)
h_e
theorem
if_simp_congr_prop: βˆ€ {b c x y u v : Prop} [inst : Decidable b] (h_c : b ↔ c), (x ↔ u) β†’ (y ↔ v) β†’ ((if b then x else y) ↔ if c then u else v)
if_simp_congr_prop
{
b: Prop
b
c: Prop
c
x: Prop
x
y: Prop
y
u: Prop
u
v: Prop
v
:
Prop: Type
Prop
} [
Decidable: Prop β†’ Type
Decidable
b: Prop
b
] (
h_c: b ↔ c
h_c
:
b: Prop
b
↔
c: Prop
c
) (
h_t: x ↔ u
h_t
:
x: Prop
x
↔
u: Prop
u
) -- FIXME: after https://github.com/leanprover/lean4/issues/1867 is fixed, -- this should be changed back to: -- (h_e : y ↔ v) : ite b x y ↔ (ite c (h := decidable_of_decidable_of_iff h_c) u v) := (
h_e: y ↔ v
h_e
:
y: Prop
y
↔
v: Prop
v
) :
ite: {Ξ± : Sort ?u.29379} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
b: Prop
b
x: Prop
x
y: Prop
y
↔ (@
ite: {Ξ± : Sort ?u.29383} β†’ (c : Prop) β†’ [h : Decidable c] β†’ Ξ± β†’ Ξ± β†’ Ξ±
ite
_: Sort ?u.29383
_
c: Prop
c
(
decidable_of_decidable_of_iff: {p q : Prop} β†’ [inst : Decidable p] β†’ (p ↔ q) β†’ Decidable q
decidable_of_decidable_of_iff
h_c: b ↔ c
h_c
)
u: Prop
u
v: Prop
v
) :=
if_ctx_simp_congr_prop: βˆ€ {b c x y u v : Prop} [inst : Decidable b] (h_c : b ↔ c), (c β†’ (x ↔ u)) β†’ (Β¬c β†’ (y ↔ v)) β†’ ((if b then x else y) ↔ if c then u else v)
if_ctx_simp_congr_prop
h_c: b ↔ c
h_c
(Ξ»
_: ?m.29449
_
=>
h_t: x ↔ u
h_t
) (Ξ»
_: ?m.29454
_
=>
h_e: y ↔ v
h_e
) -- @[congr] theorem
dif_ctx_congr: βˆ€ {Ξ± : Sort u} {b c : Prop} [dec_b : Decidable b] [dec_c : Decidable c] {x : b β†’ Ξ±} {u : c β†’ Ξ±} {y : Β¬b β†’ Ξ±} {v : Β¬c β†’ Ξ±} (h_c : b ↔ c), (βˆ€ (h : c), x (_ : b) = u h) β†’ (βˆ€ (h : Β¬c), y (_ : Β¬b) = v h) β†’ dite b x y = dite c u v
dif_ctx_congr
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
b: Prop
b
c: Prop
c
:
Prop: Type
Prop
} [
dec_b: Decidable b
dec_b
:
Decidable: Prop β†’ Type
Decidable
b: Prop
b
] [
dec_c: Decidable c
dec_c
:
Decidable: Prop β†’ Type
Decidable
c: Prop
c
] {
x: b β†’ Ξ±
x
:
b: Prop
b
β†’
Ξ±: Sort u
Ξ±
} {
u: c β†’ Ξ±
u
:
c: Prop
c
β†’
Ξ±: Sort u
Ξ±
} {
y: Β¬b β†’ Ξ±
y
: Β¬
b: Prop
b
β†’
Ξ±: Sort u
Ξ±
} {
v: Β¬c β†’ Ξ±
v
: Β¬
c: Prop
c
β†’
Ξ±: Sort u
Ξ±
} (
h_c: b ↔ c
h_c
:
b: Prop
b
↔
c: Prop
c
) (
h_t: βˆ€ (h : c), x (_ : b) = u h
h_t
: βˆ€
h: c
h
:
c: Prop
c
,
x: b β†’ Ξ±
x
(
Iff.mpr: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
Iff.mpr
h_c: b ↔ c
h_c
h: c
h
) =
u: c β†’ Ξ±
u
h: c
h
) (
h_e: βˆ€ (h : Β¬c), y (_ : Β¬b) = v h
h_e
: βˆ€
h: Β¬c
h
: Β¬
c: Prop
c
,
y: Β¬b β†’ Ξ±
y
(
Iff.mpr: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
Iff.mpr
(
not_congr: βˆ€ {a b : Prop}, (a ↔ b) β†’ (Β¬a ↔ Β¬b)
not_congr
h_c: b ↔ c
h_c
)
h: Β¬c
h
) =
v: Β¬c β†’ Ξ±
v
h: Β¬c
h
) : @
dite: {Ξ± : Sort ?u.29538} β†’ (c : Prop) β†’ [h : Decidable c] β†’ (c β†’ Ξ±) β†’ (Β¬c β†’ Ξ±) β†’ Ξ±
dite
Ξ±: Sort u
Ξ±
b: Prop
b
dec_b: Decidable b
dec_b
x: b β†’ Ξ±
x
y: Β¬b β†’ Ξ±
y
= @
dite: {Ξ± : Sort ?u.29541} β†’ (c : Prop) β†’ [h : Decidable c] β†’ (c β†’ Ξ±) β†’ (Β¬c β†’ Ξ±) β†’ Ξ±
dite
Ξ±: Sort u
Ξ±
c: Prop
c
dec_c: Decidable c
dec_c
u: c β†’ Ξ±
u
v: Β¬c β†’ Ξ±
v
:= match
dec_b: Decidable b
dec_b
,
dec_c: Decidable c
dec_c
with |
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
_,
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
hβ‚‚: Β¬c
hβ‚‚
=>
h_e: βˆ€ (h : Β¬c), y (_ : Β¬b) = v h
h_e
hβ‚‚: Β¬c
hβ‚‚
|
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
_,
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
hβ‚‚: c
hβ‚‚
=>
h_t: βˆ€ (h : c), x (_ : b) = u h
h_t
hβ‚‚: c
hβ‚‚
|
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
h₁: Β¬b
h₁
,
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
hβ‚‚: c
hβ‚‚
=>
absurd: βˆ€ {a : Prop} {b : Sort ?u.29639}, a β†’ Β¬a β†’ b
absurd
hβ‚‚: c
hβ‚‚
(
Iff.mp: βˆ€ {a b : Prop}, (a ↔ b) β†’ a β†’ b
Iff.mp
(
not_congr: βˆ€ {a b : Prop}, (a ↔ b) β†’ (Β¬a ↔ Β¬b)
not_congr
h_c: b ↔ c
h_c
)
h₁: Β¬b
h₁
) |
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
h₁: b
h₁
,
isFalse: {p : Prop} β†’ Β¬p β†’ Decidable p
isFalse
hβ‚‚: Β¬c
hβ‚‚
=>
absurd: βˆ€ {a : Prop} {b : Sort ?u.29672}, a β†’ Β¬a β†’ b
absurd
h₁: b
h₁
(
Iff.mpr: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
Iff.mpr
(
not_congr: βˆ€ {a b : Prop}, (a ↔ b) β†’ (Β¬a ↔ Β¬b)
not_congr
h_c: b ↔ c
h_c
)
hβ‚‚: Β¬c
hβ‚‚
) theorem
dif_ctx_simp_congr: βˆ€ {Ξ± : Sort u} {b c : Prop} [inst : Decidable b] {x : b β†’ Ξ±} {u : c β†’ Ξ±} {y : Β¬b β†’ Ξ±} {v : Β¬c β†’ Ξ±} (h_c : b ↔ c), (βˆ€ (h : c), x (_ : b) = u h) β†’ (βˆ€ (h : Β¬c), y (_ : Β¬b) = v h) β†’ dite b x y = dite c u v
dif_ctx_simp_congr
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
b: Prop
b
c: Prop
c
:
Prop: Type
Prop
} [
Decidable: Prop β†’ Type
Decidable
b: Prop
b
] {
x: b β†’ Ξ±
x
:
b: Prop
b
β†’
Ξ±: Sort u
Ξ±
} {
u: c β†’ Ξ±
u
:
c: Prop
c
β†’
Ξ±: Sort u
Ξ±
} {
y: Β¬b β†’ Ξ±
y
: Β¬
b: Prop
b
β†’
Ξ±: Sort u
Ξ±
} {
v: Β¬c β†’ Ξ±
v
: Β¬
c: Prop
c
β†’
Ξ±: Sort u
Ξ±
} (
h_c: b ↔ c
h_c
:
b: Prop
b
↔
c: Prop
c
) (
h_t: βˆ€ (h : c), x (_ : b) = u h
h_t
: βˆ€
h: c
h
:
c: Prop
c
,
x: b β†’ Ξ±
x
(
Iff.mpr: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
Iff.mpr
h_c: b ↔ c
h_c
h: c
h
) =
u: c β†’ Ξ±
u
h: c
h
) (
h_e: βˆ€ (h : Β¬c), y (_ : Β¬b) = v h
h_e
: βˆ€
h: Β¬c
h
: Β¬
c: Prop
c
,
y: Β¬b β†’ Ξ±
y
(
Iff.mpr: βˆ€ {a b : Prop}, (a ↔ b) β†’ b β†’ a
Iff.mpr
(
not_congr: βˆ€ {a b : Prop}, (a ↔ b) β†’ (Β¬a ↔ Β¬b)
not_congr
h_c: b ↔ c
h_c
)
h: Β¬c
h
) =
v: Β¬c β†’ Ξ±
v
h: Β¬c
h
) : -- FIXME: after https://github.com/leanprover/lean4/issues/1867 is fixed, -- this should be changed back to: -- dite b x y = dite c (h := decidable_of_decidable_of_iff h_c) u v :=
dite: {Ξ± : Sort ?u.29923} β†’ (c : Prop) β†’ [h : Decidable c] β†’ (c β†’ Ξ±) β†’ (Β¬c β†’ Ξ±) β†’ Ξ±
dite
b: Prop
b
x: b β†’ Ξ±
x
y: Β¬b β†’ Ξ±
y
= @
dite: {Ξ± : Sort ?u.29933} β†’ (c : Prop) β†’ [h : Decidable c] β†’ (c β†’ Ξ±) β†’ (Β¬c β†’ Ξ±) β†’ Ξ±
dite
_: Sort ?u.29933
_
c: Prop
c
(
decidable_of_decidable_of_iff: {p q : Prop} β†’ [inst : Decidable p] β†’ (p ↔ q) β†’ Decidable q
decidable_of_decidable_of_iff
h_c: b ↔ c
h_c
)
u: c β†’ Ξ±
u
v: Β¬c β†’ Ξ±
v
:=
dif_ctx_congr: βˆ€ {Ξ± : Sort ?u.29991} {b c : Prop} [dec_b : Decidable b] [dec_c : Decidable c] {x : b β†’ Ξ±} {u : c β†’ Ξ±} {y : Β¬b β†’ Ξ±} {v : Β¬c β†’ Ξ±} (h_c : b ↔ c), (βˆ€ (h : c), x (_ : b) = u h) β†’ (βˆ€ (h : Β¬c), y (_ : Β¬b) = v h) β†’ dite b x y = dite c u v
dif_ctx_congr
(dec_c :=
decidable_of_decidable_of_iff: {p q : Prop} β†’ [inst : Decidable p] β†’ (p ↔ q) β†’ Decidable q
decidable_of_decidable_of_iff
h_c: b ↔ c
h_c
)
h_c: b ↔ c
h_c
h_t: βˆ€ (h : c), x (_ : b) = u h
h_t
h_e: βˆ€ (h : Β¬c), y (_ : Β¬b) = v h
h_e
def
AsTrue: (c : Prop) β†’ [inst : Decidable c] β†’ Prop
AsTrue
(
c: Prop
c
:
Prop: Type
Prop
) [
Decidable: Prop β†’ Type
Decidable
c: Prop
c
] :
Prop: Type
Prop
:= if
c: Prop
c
then
True: Prop
True
else
False: Prop
False
def
AsFalse: (c : Prop) β†’ [inst : Decidable c] β†’ Prop
AsFalse
(
c: Prop
c
:
Prop: Type
Prop
) [
Decidable: Prop β†’ Type
Decidable
c: Prop
c
] :
Prop: Type
Prop
:= if
c: Prop
c
then
False: Prop
False
else
True: Prop
True
theorem
AsTrue.get: βˆ€ {c : Prop} [h₁ : Decidable c], AsTrue c β†’ c
AsTrue.get
{
c: Prop
c
:
Prop: Type
Prop
} [
h₁: Decidable c
h₁
:
Decidable: Prop β†’ Type
Decidable
c: Prop
c
] (
_: AsTrue c
_
:
AsTrue: (c : Prop) β†’ [inst : Decidable c] β†’ Prop
AsTrue
c: Prop
c
) :
c: Prop
c
:= match
h₁: Decidable c
h₁
with |
isTrue: {p : Prop} β†’ p β†’ Decidable p
isTrue
h_c: c
h_c
=>
h_c: c
h_c
#align of_as_true
AsTrue.get: βˆ€ {c : Prop} [h₁ : Decidable c], AsTrue c β†’ c
AsTrue.get
#align ulift
ULift: Type s β†’ Type (maxsr)
ULift
#align ulift.up
ULift.up: {Ξ± : Type s} β†’ Ξ± β†’ ULift Ξ±
ULift.up
#align ulift.down
ULift.down: {Ξ± : Type s} β†’ ULift Ξ± β†’ Ξ±
ULift.down
#align plift
PLift: Sort u β†’ Type u
PLift
#align plift.up
PLift.up: {Ξ± : Sort u} β†’ Ξ± β†’ PLift Ξ±
PLift.up
#align plift.down
PLift.down: {Ξ± : Sort u} β†’ PLift Ξ± β†’ Ξ±
PLift.down
/- Equalities for rewriting let-expressions -/ theorem
let_value_eq: βˆ€ {Ξ± : Sort u} {Ξ² : Sort v} {a₁ aβ‚‚ : Ξ±} (b : Ξ± β†’ Ξ²), a₁ = aβ‚‚ β†’ (let x := a₁; b x) = let x := aβ‚‚; b x
let_value_eq
{
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
Ξ²: Sort v
Ξ²
:
Sort v: Type v
Sort
Sort v: Type v
v
} {
a₁: Ξ±
a₁
aβ‚‚: Ξ±
aβ‚‚
:
Ξ±: Sort u
Ξ±
} (
b: Ξ± β†’ Ξ²
b
:
Ξ±: Sort u
Ξ±
β†’
Ξ²: Sort v
Ξ²
) (
h: a₁ = aβ‚‚
h
:
a₁: Ξ±
a₁
=
aβ‚‚: Ξ±
aβ‚‚
) : (let
x: Ξ±
x
:
Ξ±: Sort u
Ξ±
:=
a₁: Ξ±
a₁
;
b: Ξ± β†’ Ξ²
b
x: Ξ±
x
) = (let
x: Ξ±
x
:
Ξ±: Sort u
Ξ±
:=
aβ‚‚: Ξ±
aβ‚‚
;
b: Ξ± β†’ Ξ²
b
x: Ξ±
x
) :=
congrArg: βˆ€ {Ξ± : Sort ?u.30363} {Ξ² : Sort ?u.30362} {a₁ aβ‚‚ : Ξ±} (f : Ξ± β†’ Ξ²), a₁ = aβ‚‚ β†’ f a₁ = f aβ‚‚
congrArg
b: Ξ± β†’ Ξ²
b
h: a₁ = aβ‚‚
h
theorem
let_value_heq: βˆ€ {Ξ± : Sort v} {Ξ² : Ξ± β†’ Sort u} {a₁ aβ‚‚ : Ξ±} (b : (x : Ξ±) β†’ Ξ² x), a₁ = aβ‚‚ β†’ HEq (let x := a₁; b x) (let x := aβ‚‚; b x)
let_value_heq
{
Ξ±: Sort v
Ξ±
:
Sort v: Type v
Sort
Sort v: Type v
v
} {
Ξ²: Ξ± β†’ Sort u
Ξ²
:
Ξ±: Sort v
Ξ±
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} {
a₁: Ξ±
a₁
aβ‚‚: Ξ±
aβ‚‚
:
Ξ±: Sort v
Ξ±
} (
b: (x : Ξ±) β†’ Ξ² x
b
: βˆ€
x: Ξ±
x
:
Ξ±: Sort v
Ξ±
,
Ξ²: Ξ± β†’ Sort u
Ξ²
x: Ξ±
x
) (
h: a₁ = aβ‚‚
h
:
a₁: Ξ±
a₁
=
aβ‚‚: Ξ±
aβ‚‚
) :
HEq: {Ξ± : Sort ?u.30416} β†’ Ξ± β†’ {Ξ² : Sort ?u.30416} β†’ Ξ² β†’ Prop
HEq
(let
x: Ξ±
x
:
Ξ±: Sort v
Ξ±
:=
a₁: Ξ±
a₁
;
b: (x : Ξ±) β†’ Ξ² x
b
x: Ξ±
x
) (let
x: Ξ±
x
:
Ξ±: Sort v
Ξ±
:=
aβ‚‚: Ξ±
aβ‚‚
;
b: (x : Ξ±) β†’ Ξ² x
b
x: Ξ±
x
) :=

Goals accomplished! πŸ™
a, b✝, c, d: Prop

p: ?m.30394

Ξ±: Sort v

Ξ²: Ξ± β†’ Sort u

a₁, aβ‚‚: Ξ±

b: (x : Ξ±) β†’ Ξ² x

h: a₁ = aβ‚‚


HEq (let x := a₁; b x) (let x := aβ‚‚; b x)
a, b✝, c, d: Prop

p: ?m.30394

Ξ±: Sort v

Ξ²: Ξ± β†’ Sort u

a₁: Ξ±

b: (x : Ξ±) β†’ Ξ² x


refl
HEq (let x := a₁; b x) (let x := a₁; b x)
a, b✝, c, d: Prop

p: ?m.30394

Ξ±: Sort v

Ξ²: Ξ± β†’ Sort u

a₁: Ξ±

b: (x : Ξ±) β†’ Ξ² x


refl
HEq (let x := a₁; b x) (let x := a₁; b x)
a, b✝, c, d: Prop

p: ?m.30394

Ξ±: Sort v

Ξ²: Ξ± β†’ Sort u

a₁, aβ‚‚: Ξ±

b: (x : Ξ±) β†’ Ξ² x

h: a₁ = aβ‚‚


HEq (let x := a₁; b x) (let x := aβ‚‚; b x)

Goals accomplished! πŸ™
#align let_value_heq
let_value_heq: βˆ€ {Ξ± : Sort v} {Ξ² : Ξ± β†’ Sort u} {a₁ aβ‚‚ : Ξ±} (b : (x : Ξ±) β†’ Ξ² x), a₁ = aβ‚‚ β†’ HEq (let x := a₁; b x) (let x := aβ‚‚; b x)
let_value_heq
-- FIXME: mathport thinks this is a dubious translation theorem
let_body_eq: βˆ€ {Ξ± : Sort v} {Ξ² : Ξ± β†’ Sort u} (a : Ξ±) {b₁ bβ‚‚ : (x : Ξ±) β†’ Ξ² x}, (βˆ€ (x : Ξ±), b₁ x = bβ‚‚ x) β†’ (let x := a; b₁ x) = let x := a; bβ‚‚ x
let_body_eq
{
Ξ±: Sort v
Ξ±
:
Sort v: Type v
Sort
Sort v: Type v
v
} {
Ξ²: Ξ± β†’ Sort u
Ξ²
:
Ξ±: Sort v
Ξ±
β†’
Sort u: Type u
Sort
Sort u: Type u
u
} (
a: Ξ±
a
:
Ξ±: Sort v
Ξ±
) {
b₁: (x : Ξ±) β†’ Ξ² x
b₁
bβ‚‚: (x : Ξ±) β†’ Ξ² x
bβ‚‚
: βˆ€
x: Ξ±
x
:
Ξ±: Sort v
Ξ±
,
Ξ²: Ξ± β†’ Sort u
Ξ²
x: Ξ±
x
} (
h: βˆ€ (x : Ξ±), b₁ x = bβ‚‚ x
h
: βˆ€
x: ?m.30572
x
,
b₁: (x : Ξ±) β†’ Ξ² x
b₁
x: ?m.30572
x
=
bβ‚‚: (x : Ξ±) β†’ Ξ² x
bβ‚‚
x: ?m.30572
x
) : (let
x: Ξ±
x
:
Ξ±: Sort v
Ξ±
:=
a: Ξ±
a
;
b₁: (x : Ξ±) β†’ Ξ² x
b₁
x: Ξ±
x
) = (let
x: Ξ±
x
:
Ξ±: Sort v
Ξ±
:=
a: Ξ±
a
;
bβ‚‚: (x : Ξ±) β†’ Ξ² x
bβ‚‚
x: Ξ±
x
) :=

Goals accomplished! πŸ™
a✝, b, c, d: Prop

p: ?m.30550

Ξ±: Sort v

Ξ²: Ξ± β†’ Sort u

a: Ξ±

b₁, bβ‚‚: (x : Ξ±) β†’ Ξ² x

h: βˆ€ (x : Ξ±), b₁ x = bβ‚‚ x


(let x := a; b₁ x) = let x := a; bβ‚‚ x

Goals accomplished! πŸ™
#align let_value_eq
let_value_eq: βˆ€ {Ξ± : Sort u} {Ξ² : Sort v} {a₁ aβ‚‚ : Ξ±} (b : Ξ± β†’ Ξ²), a₁ = aβ‚‚ β†’ (let x := a₁; b x) = let x := aβ‚‚; b x
let_value_eq
-- FIXME: mathport thinks this is a dubious translation theorem
let_eq: βˆ€ {Ξ± : Sort v} {Ξ² : Sort u} {a₁ aβ‚‚ : Ξ±} {b₁ bβ‚‚ : Ξ± β†’ Ξ²}, a₁ = aβ‚‚ β†’ (βˆ€ (x : Ξ±), b₁ x = bβ‚‚ x) β†’ (let x := a₁; b₁ x) = let x := aβ‚‚; bβ‚‚ x
let_eq
{
Ξ±: Sort v
Ξ±
:
Sort v: Type v
Sort
Sort v: Type v
v
} {
Ξ²: Sort u
Ξ²
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
a₁: Ξ±
a₁
aβ‚‚: Ξ±
aβ‚‚
:
Ξ±: Sort v
Ξ±
} {
b₁: Ξ± β†’ Ξ²
b₁
bβ‚‚: Ξ± β†’ Ξ²
bβ‚‚
:
Ξ±: Sort v
Ξ±
β†’
Ξ²: Sort u
Ξ²
} (
h₁: a₁ = aβ‚‚
h₁
:
a₁: Ξ±
a₁
=
aβ‚‚: Ξ±
aβ‚‚
) (
hβ‚‚: βˆ€ (x : Ξ±), b₁ x = bβ‚‚ x
hβ‚‚
: βˆ€
x: ?m.30661
x
,
b₁: Ξ± β†’ Ξ²
b₁
x: ?m.30661
x
=
bβ‚‚: Ξ± β†’ Ξ²
bβ‚‚
x: ?m.30661
x
) : (let
x: Ξ±
x
:
Ξ±: Sort v
Ξ±
:=
a₁: Ξ±
a₁
;
b₁: Ξ± β†’ Ξ²
b₁
x: Ξ±
x
) = (let
x: Ξ±
x
:
Ξ±: Sort v
Ξ±
:=
aβ‚‚: Ξ±
aβ‚‚
;
bβ‚‚: Ξ± β†’ Ξ²
bβ‚‚
x: Ξ±
x
) :=

Goals accomplished! πŸ™
a, b, c, d: Prop

p: ?m.30637

Ξ±: Sort v

Ξ²: Sort u

a₁, aβ‚‚: Ξ±

b₁, bβ‚‚: Ξ± β†’ Ξ²

h₁: a₁ = aβ‚‚

hβ‚‚: βˆ€ (x : Ξ±), b₁ x = bβ‚‚ x


(let x := a₁; b₁ x) = let x := aβ‚‚; bβ‚‚ x

Goals accomplished! πŸ™
#align let_eq
let_eq: βˆ€ {Ξ± : Sort v} {Ξ² : Sort u} {a₁ aβ‚‚ : Ξ±} {b₁ bβ‚‚ : Ξ± β†’ Ξ²}, a₁ = aβ‚‚ β†’ (βˆ€ (x : Ξ±), b₁ x = bβ‚‚ x) β†’ (let x := a₁; b₁ x) = let x := aβ‚‚; bβ‚‚ x
let_eq
-- FIXME: mathport thinks this is a dubious translation section Relation variable {
Ξ±: Sort u
Ξ±
:
Sort u: Type u
Sort
Sort u: Type u
u
} {
Ξ²: Sort v
Ξ²
:
Sort v: Type v
Sort
Sort v: Type v
v
} (
r: Ξ² β†’ Ξ² β†’ Prop
r
:
Ξ²: Sort v
Ξ²
β†’
Ξ²: Sort v
Ξ²
β†’
Prop: Type
Prop
) /-- Local notation for an arbitrary binary relation `r`. -/ local infix:50 " β‰Ί " => r /-- A reflexive relation relates every element to itself. -/ def
Reflexive: ?m.32893
Reflexive
:= βˆ€
x: ?m.32896
x
,
x: ?m.32896
x
β‰Ί
x: ?m.32896
x
/-- A relation is symmetric if `x β‰Ί y` implies `y β‰Ί x`. -/ def
Symmetric: ?m.32932
Symmetric
:= βˆ€ ⦃
x: ?m.32935
x
y: ?m.32938
y
⦄,
x: ?m.32935
x
β‰Ί
y: ?m.32938
y
β†’
y: ?m.32938
y
β‰Ί
x: ?m.32935
x
/-- A relation is transitive if `x β‰Ί y` and `y β‰Ί z` together imply `x β‰Ί z`. -/ def
Transitive: ?m.32982
Transitive
:= βˆ€ ⦃
x: ?m.32985
x
y: ?m.32988
y
z: ?m.32991
z
⦄,
x: ?m.32985
x
β‰Ί
y: ?m.32988
y
β†’
y: ?m.32988
y
β‰Ί
z: ?m.32991
z
β†’
x: ?m.32985
x
β‰Ί
z: ?m.32991
z
lemma
Equivalence.reflexive: βˆ€ {r : Ξ² β†’ Ξ² β†’ Prop}, Equivalence r β†’ Reflexive r
Equivalence.reflexive
{
r: Ξ² β†’ Ξ² β†’ Prop
r
:
Ξ²: Sort v
Ξ²
β†’
Ξ²: Sort v
Ξ²
β†’
Prop: Type
Prop
} (h :
Equivalence: {Ξ± : Sort ?u.33049} β†’ (Ξ± β†’ Ξ± β†’ Prop) β†’ Prop
Equivalence
r: Ξ² β†’ Ξ² β†’ Prop
r
) :
Reflexive: {Ξ² : Sort ?u.33059} β†’ (Ξ² β†’ Ξ² β†’ Prop) β†’ Prop
Reflexive
r: Ξ² β†’ Ξ² β†’ Prop
r
:= h.
refl: βˆ€ {Ξ± : Sort ?u.33072} {r : Ξ± β†’ Ξ± β†’ Prop}, Equivalence r β†’ βˆ€ (x : Ξ±), r x x
refl
lemma
Equivalence.symmetric: βˆ€ {Ξ² : Sort v} {r : Ξ² β†’ Ξ² β†’ Prop}, Equivalence r β†’ Symmetric r
Equivalence.symmetric
{
r: Ξ² β†’ Ξ² β†’ Prop
r
:
Ξ²: Sort v
Ξ²
β†’
Ξ²: Sort v
Ξ²
β†’
Prop: Type
Prop
} (h :
Equivalence: {Ξ± : Sort ?u.33115} β†’ (Ξ± β†’ Ξ± β†’ Prop) β†’ Prop
Equivalence
r: Ξ² β†’ Ξ² β†’ Prop
r
) :
Symmetric: {Ξ² : Sort ?u.33125} β†’ (Ξ² β†’ Ξ² β†’ Prop) β†’ Prop
Symmetric
r: Ξ² β†’ Ξ² β†’ Prop
r
:= Ξ»
_: ?m.33139
_
_: ?m.33142
_
=> h.
symm: βˆ€ {Ξ± : Sort ?u.33144} {r : Ξ± β†’ Ξ± β†’ Prop}, Equivalence r β†’ βˆ€ {x y : Ξ±}, r x y β†’ r y x
symm
lemma
Equivalence.transitive: βˆ€ {r : Ξ² β†’ Ξ² β†’ Prop}, Equivalence r β†’ Transitive r
Equivalence.transitive
{
r: Ξ² β†’ Ξ² β†’ Prop
r
:
Ξ²: Sort v
Ξ²
β†’
Ξ²: Sort v
Ξ²
β†’
Prop: Type
Prop
}(h :
Equivalence: {Ξ± : Sort ?u.33197} β†’ (Ξ± β†’ Ξ± β†’ Prop) β†’ Prop
Equivalence
r: Ξ² β†’ Ξ² β†’ Prop
r
) :
Transitive: {Ξ² : Sort ?u.33207} β†’ (Ξ² β†’ Ξ² β†’ Prop) β†’ Prop
Transitive
r: Ξ² β†’ Ξ² β†’ Prop
r
:= Ξ»
_: ?m.33221
_
_: ?m.33224
_
_: ?m.33227
_
=> h.
trans: βˆ€ {Ξ± : Sort ?u.33229} {r : Ξ± β†’ Ξ± β†’ Prop}, Equivalence r β†’ βˆ€ {x y z : Ξ±}, r x y β†’ r y z β†’ r x z
trans
/-- A relation is total if for all `x` and `y`, either `x β‰Ί y` or `y β‰Ί x`. -/ def
Total: ?m.33282
Total
:= βˆ€
x: ?m.33285
x
y: ?m.33288
y
,
x: ?m.33285
x
β‰Ί
y: ?m.33288
y
∨
y: ?m.33288
y
β‰Ί
x: ?m.33285
x
#align mk_equivalence
Equivalence.mk: βˆ€ {Ξ± : Sort u} {r : Ξ± β†’ Ξ± β†’ Prop}, (βˆ€ (x : Ξ±), r x x) β†’ (βˆ€ {x y : Ξ±}, r x y β†’ r y x) β†’ (βˆ€ {x y z : Ξ±}, r x y β†’ r y z β†’ r x z) β†’ Equivalence r
Equivalence.mk
/-- Irreflexive means "not reflexive". -/ def
Irreflexive: {Ξ² : Sort v} β†’ (Ξ² β†’ Ξ² β†’ Prop) β†’ Prop
Irreflexive
:= βˆ€
x: ?m.33330
x
, Β¬
x: ?m.33330
x
β‰Ί
x: ?m.33330
x
/-- A relation is antisymmetric if `x β‰Ί y` and `y β‰Ί x` together imply that `x = y`. -/ def
AntiSymmetric: ?m.33366
AntiSymmetric
:= βˆ€ ⦃
x: ?m.33369
x
y: ?m.33372
y
⦄,
x: ?m.33369
x
β‰Ί
y: ?m.33372
y
β†’
y: ?m.33372
y