Theorems · Theorem · logic and foundations
of_not_not
∀ {a : Prop}, ¬¬a → a- Defined in
- Mathlib.Logic.Basic
- Cited by
- 51 results in Mathlib
- Foundations
- Depth 14 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- by_contraproof · cited by 60
Cited by51
Results whose statement or proof uses this declaration.
- CharP.existsproof · cited by 16
- WfDvdMonoid.exists_irreducible_factorproof · cited by 12
- Set.Pairwise.eqproof · cited by 12
- IsSeparable.isIntegralproof · cited by 8
- specializes_TFAEproof · cited by 6
- MeasureTheory.measure_le_setAverage_posproof · cited by 5
- isAddTorsionFree_iff_not_isOfFinAddOrderproof · cited by 4
- isMin_iff_forall_not_ltproof · cited by 4
- Equiv.Perm.IsCycle.extendDomainproof · cited by 3
- MeasureTheory.measure_eq_top_of_lintegral_ne_topproof · cited by 3
- Ideal.exists_ideal_comap_le_primeproof · cited by 3
- Flag.mem_iff_forall_le_or_geproof · cited by 3