Mathlib Map

Theorems · Theorem · order theory

lt_of_one_div_lt_one_div

∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < a → 1 / a < 1 / b → b < a
Defined in
Mathlib.Algebra.Order.Field.Basic
Cited by
1 results in Mathlib
Foundations
Depth 47 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes
SemifieldPartialOrderPosMulReflectLT
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

MeasureTheory.eLpNorm_le_eLpNorm_mul_eLpNorm_of_nnnorm · cited by 4MeasureTheory.eLpNorm_le_…PartialOrder · cited by 6410PartialOrderone_mul · cited by 2841one_mulone_div · cited by 624one_divSemifield · cited by 439SemifieldPosMulReflectLT · cited by 278PosMulReflectLTdiv_inv_eq_mul · cited by 53div_inv_eq_mulone_div_lt_one_div_of_lt · cited by 2one_div_lt_one_div_of_ltlt_of_one_div_lt_one_divCITED BYCITES

Cites7

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

Cited by1

Results whose statement or proof uses this declaration.