Mathlib Map

Theorems · Theorem · logic and foundations

Fact.elim

∀ {p : Prop}, Fact p → p
Defined in
Mathlib.Logic.Basic
Cited by
25 results in Mathlib
Foundations
Depth 2 from the axioms · uses no axioms
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

MeasureTheory.integrableOn_condExpL2_of_measure_ne_top · cited by 5MeasureTheory.integrableO…MeasureTheory.Lp.induction · cited by 5Lp.inductionorthonormal_fourier · cited by 3orthonormal_fourierMeasureTheory.integral_condExpL2_eq · cited by 3MeasureTheory.integral_co…Equiv.Perm.pow_prime_eq_one_iff · cited by 2Perm.pow_prime_eq_one_ifflp.sum_rpow_le_of_tendsto · cited by 2lp.sum_rpow_le_of_tendstoexists_orderOf_eq_prime_pow_iff · cited by 2exists_orderOf_eq_prime_p…MeasureTheory.L2.inner_indicatorConstLp_eq_inner_setIntegral · cited by 2L2.inner_indicatorConstLp…MeasureTheory.lintegral_nnnorm_condExpL2_le · cited by 2MeasureTheory.lintegral_n…exists_addOrderOf_eq_prime_pow_iff · cited by 2exists_addOrderOf_eq_prim…Rat.AbsoluteValue.equiv_padic_of_bounded · cited by 1AbsoluteValue.equiv_padic…fourierSubalgebra_separatesPoints · cited by 1fourierSubalgebra_separat…padicValNat_factorial_lt_of_ne_zero · cited by 1padicValNat_factorial_lt_…MeasureTheory.condExpL2_comp_continuousLinearMap · cited by 1MeasureTheory.condExpL2_c…MeasureTheory.MemLp.induction · cited by 1MemLp.inductionFact · cited by 2726FactFact.out · cited by 328Fact.outFact.elimCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Factstatement and proof · cited by 2,726
  • Fact.outproof · cited by 328

Cited by25

Results whose statement or proof uses this declaration.