Theorems · Theorem · logic and foundations
Not.imp_symm
∀ {a b : Prop}, (¬a → b) → ¬b → a- Defined in
- Mathlib.Logic.Basic
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 12 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.
- Not.decidable_imp_symmproof · cited by 2
Cited by25
Results whose statement or proof uses this declaration.
- MeasureTheory.Integrable.of_integral_ne_zeroproof · cited by 8
- Finset.sum_preimageproof · cited by 6
- Finset.prod_preimageproof · cited by 4
- Submodule.mem_of_localization_maximalproof · cited by 4
- Set.support_indicator_subsetproof · cited by 4
- DFinsupp.Lex.wellFounded'proof · cited by 3
- maximal_orthonormal_iff_orthogonalComplement_eq_botproof · cited by 3
- Nat.factorization_choose_le_logproof · cited by 3
- Set.mulSupport_mulIndicator_subsetproof · cited by 3
- Ideal.ramificationIdx'_le_ramificationIdx'proof · cited by 2
- SimpleGraph.preconnected_of_ediam_ne_topproof · cited by 1
- FormalMultilinearSeries.changeOrigin_eval_of_finiteproof · cited by 1