instance
instDecidablePredComp_batteries
{α : Sort u_1}
{β : Sort u_2}
{p : β → Prop}
{f : α → β}
[DecidablePred p]
:
DecidablePred (p ∘ f)
Equations
- instDecidablePredComp_batteries = inferInstanceAs (DecidablePred fun (x : α) => p (f x))
@[deprecated proof_irrel]
Alias of proof_irrel
.
id #
decidable #
theorem
Decidable.exists_not_of_not_forall
{α : Sort u_1}
{p : α → Prop}
[Decidable (∃ (x : α), ¬p x)]
[(x : α) → Decidable (p x)]
:
Alias of the forward direction of Decidable.not_forall
.
classical logic #
Alias of the forward direction of Classical.not_forall
.
equality #
@[deprecated funext_iff]
Alias of funext_iff
.
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
miscellaneous #
If all points are equal to a given point x
, then α
is a subsingleton.