Theorems · Theorem · order theory
max_le_iff
∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, max a b ≤ c ↔ a ≤ c ∧ b ≤ c- Defined in
- Mathlib.Order.MinMax
- Cited by
- 25 results in Mathlib
- Foundations
- Depth 17 from the axioms · uses propext
- Assumes
- LinearOrder
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites2
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
- sup_le_iffproof · cited by 58
Cited by25
Results whose statement or proof uses this declaration.
- max_le_add_of_nonnegproof · cited by 6
- Finset.fold_max_leproof · cited by 4
- rank_fun_infiniteproof · cited by 2
- Filter.comap_abs_atTopproof · cited by 2
- Cardinal.ciSup_addproof · cited by 2
- Cardinal.ciSup_mulproof · cited by 2
- isBigO_norm_Icc_restrict_atTopproof · cited by 2
- IsNonarchimedean.add_leproof · cited by 1
- Metric.hausdorffEDist_le_of_mem_hausdorffEntourageproof · cited by 1
- Bornology.IsBounded.uniformContinuousOn_smulproof · cited by 1
- List.max_prod_leproof · cited by 1
- List.max_sum_leproof · cited by 1