Mathlib Map

Theorems · Theorem · order theory

GT.gt.lt

∀ {α : Type u_2} [inst : LT α] {a b : α}, a > b → b < a
Defined in
Mathlib.Order.Basic
Cited by
16 results in Mathlib
Foundations
Depth 3 from the axioms · uses no axioms
Assumes
LT
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Complex.exp_zero · cited by 43Complex.exp_zeroFunction.minimalPeriod_pos_of_mem_periodicPts · cited by 9Function.minimalPeriod_po…FormalMultilinearSeries.norm_mul_pow_le_of_lt_radius · cited by 6FormalMultilinearSeries.n…MeasureTheory.lintegral_comp_eq_lintegral_meas_le_mul · cited by 3MeasureTheory.lintegral_c…ContinuousMap.idealOfSet_ofIdeal_eq_closure · cited by 2ContinuousMap.idealOfSet_…ContinuousLinearMap.exists_nonlinearRightInverse_of_surjective · cited by 2ContinuousLinearMap.exist…uniformCauchySeqOn_ball_of_fderiv · cited by 2uniformCauchySeqOn_ball_o…AnalyticAt.eventually_constant_or_nhds_le_map_nhds_aux · cited by 1AnalyticAt.eventually_con…FormalMultilinearSeries.nnnorm_mul_pow_le_of_lt_radius · cited by 1FormalMultilinearSeries.n…Complex.liouville_theorem_aux · cited by 1Complex.liouville_theorem…uniformCauchySeqOnFilter_of_fderiv · cited by 1uniformCauchySeqOnFilter_…hasFPowerSeriesAt_iff · cited by 1hasFPowerSeriesAt_iffBoxIntegral.HasIntegral.of_aeEq_zero · cited by 1HasIntegral.of_aeEq_zeroLocallyFinite.exists_forall_eventually_eq_prod · cited by 1LocallyFinite.exists_fora…MeasureTheory.Conservative.measure_mem_forall_ge_image_notMem_eq_zero · cited by 1Conservative.measure_mem_…gt.ltCITED BYCITES

Cites0

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

Nothing in Mathlib beyond the foundations.

Cited by16

Results whose statement or proof uses this declaration.