Theorems · Theorem · field theory
LinearOrderedField.cutMap_bddAbove
∀ {α : Type u_2} (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
[inst_4 : LinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (a : α), BddAbove (LinearOrderedField.cutMap β a)- Defined in
- Mathlib.Algebra.Order.CompleteField
- Cited by
- 4 results in Mathlib
- Foundations
- Depth 86 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- LinearOrderstatement and proof · cited by 8,572
- Fieldstatement and proof · cited by 7,404
- Set.ofPredproof · cited by 6,101
- IsStrictOrderedRingstatement and proof · cited by 2,490
- LT.lt.leproof · cited by 2,189
- BddAbovestatement · cited by 620
- Archimedeanstatement and proof · cited by 603
- Set.forall_mem_imageproof · cited by 65
- LT.lt.trans'proof · cited by 15
- LinearOrderedField.cutMapstatement · cited by 13
- exists_rat_gtproof · cited by 10
Cited by4
Results whose statement or proof uses this declaration.
- ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iffproof · cited by 4
- ConditionallyCompleteLinearOrderedField.inducedMap_monoproof · cited by 3
- ConditionallyCompleteLinearOrderedField.inducedMap_addproof · cited by 1