Implication →
is transitive. If P → Q
and Q → R
then P → R
.
Alias of congrArg
.
Congruence in the function argument: if a₁ = a₂
then f a₁ = f a₂
for
any (nondependent) function f
. This is more powerful than it might look at first, because
you can also use a lambda expression for f
to prove that
<something containing a₁> = <something containing a₂>
. This function is used
internally by tactics like congr
and simp
to apply equalities inside
subterms.
For more information: Equality
Alias of the forward direction of not_not_not
.
Pretty-printing for ExistsUnique
, following the same pattern as pretty printing
for Exists
.
Instances For
Instances For
Instances For
Alias of Decidable.byCases
.
Synonym for dite
(dependent if-then-else). We can construct an element q
(of any sort, not just a proposition) by cases on whether p
is true or false,
provided p
is decidable.
Instances For
Alias of Decidable.byContradiction
.
Alias of instDecidableOr
.
Instances For
Alias of instDecidableAnd
.
Instances For
Alias of instDecidableNot
.
Instances For
Alias of instDecidableIff
.
Instances For
Instances For
A relation is transitive if x ≺ y
and y ≺ z
together imply x ≺ z
.
Instances For
Irreflexive means "not reflexive".
Instances For
A relation is antisymmetric if x ≺ y
and y ≺ x
together imply that x = y
.
Instances For
An empty relation does not relate any elements.