Equations
- instTransPropIff = { trans := @instTransPropIff.proof_1 }
Alias of the forward direction of not_not_not
.
Equations
- ExistsUnique p = ∃ x, p x ∧ ∀ (y : α), p y → y = x
Equations
- One or more equations did not get rendered due to their size.
Pretty-printing for ExistsUnique
, following the same pattern as pretty printing
for Exists
.
Equations
- One or more equations did not get rendered due to their size.
def
Decidable.recOn_true
(p : Prop)
[h : Decidable p]
{h₁ : p → Sort u}
{h₂ : ¬p → Sort u}
(h₃ : p)
(h₄ : h₁ h₃)
:
Decidable.recOn h h₂ h₁
Equations
- Decidable.recOn_true p h₃ h₄ = cast (_ : h₁ h₃ = Decidable.recOn h h₂ h₁) h₄
def
Decidable.recOn_false
(p : Prop)
[h : Decidable p]
{h₁ : p → Sort u}
{h₂ : ¬p → Sort u}
(h₃ : ¬p)
(h₄ : h₂ h₃)
:
Decidable.recOn h h₂ h₁
Equations
- Decidable.recOn_false p h₃ h₄ = cast (_ : h₂ h₃ = Decidable.recOn h h₂ h₁) h₄
Alias of Decidable.byCases
.
Equations
Alias of Decidable.byContradiction
.
Alias of Decidable.not_not
.
Alias of instDecidableOr
.
Equations
Alias of instDecidableAnd
.
Equations
Alias of instDecidableNot
.
Equations
Alias of instDecidableIff
.
Equations
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₁)
A relation is transitive if x ≺ y≺ y
and y ≺ z≺ z
together imply x ≺ z≺ z
.
Equations
- Transitive r = (⦃x y z : β⦄ → r x y → r y z → r x z)
Irreflexive means "not reflexive".
Equations
- Irreflexive r = ∀ (x : β), ¬r x x
A relation is antisymmetric if x ≺ y≺ y
and y ≺ x≺ x
together imply that x = y
.
Equations
- AntiSymmetric r = ∀ ⦃x y : β⦄, r x y → r y x → x = y
An empty relation does not relate any elements.
Equations
- EmptyRelation x x = False
theorem
InvImage.trans
{α : Sort u}
{β : Sort v}
(r : β → β → Prop)
(f : α → β)
(h : Transitive r)
:
Transitive (InvImage r f)
theorem
InvImage.irreflexive
{α : Sort u}
{β : Sort v}
(r : β → β → Prop)
(f : α → β)
(h : Irreflexive r)
:
Irreflexive (InvImage r f)
Equations
- Commutative f = ∀ (a b : α), f a b = f b a
Equations
- Associative f = ∀ (a b c : α), f (f a b) c = f a (f b c)
Equations
- LeftIdentity f one = ∀ (a : α), f one a = a
Equations
- RightIdentity f one = ∀ (a : α), f a one = a
Equations
- RightInverse f inv one = ∀ (a : α), f a (inv a) = one
Equations
- LeftCancelative f = ∀ (a b c : α), f a b = f a c → b = c
Equations
- RightCancelative f = ∀ (a b c : α), f a b = f c b → a = c
Equations
- LeftDistributive f g = ∀ (a b c : α), f a (g b c) = g (f a b) (f a c)
Equations
- RightDistributive f g = ∀ (a b c : α), f (g a b) c = g (f a c) (f b c)
Equations
- RightCommutative h = ∀ (b : β) (a₁ a₂ : α), h (h b a₁) a₂ = h (h b a₂) a₁
Equations
- LeftCommutative h = ∀ (a₁ a₂ : α) (b : β), h a₁ (h a₂ b) = h a₂ (h a₁ b)
unsafe def
WellFounded.fix'.impl
{α : Sort u}
{C : α → Sort v}
{r : α → α → Prop}
(hwf : WellFounded r)
(F : (x : α) → ((y : α) → r y x → C y) → C x)
(x : α)
:
C x
Equations
- WellFounded.fix'.impl hwf F x = F x fun y x => WellFounded.fix'.impl hwf F y
@[implemented_by WellFounded.fix'.impl]
def
WellFounded.fix'
{α : Sort u}
{C : α → Sort v}
{r : α → α → Prop}
(hwf : WellFounded r)
(F : (x : α) → ((y : α) → r y x → C y) → C x)
(x : α)
:
C x
Equations
- WellFounded.fix' hwf F x = WellFounded.fix hwf F x