Theorems / mh_ineq_a0ad18
Mathlib held-out
Inequalities · medium
theorem lg_target {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Set α} {a ε : α} (h : IsLUB s a) (hε : 0 < ε) : ∃ b ∈ s, a - ε < b ∧ b ≤ a := by- Mathlib declaration
- IsLUB.exists_between_sub_self
- Held-out module
- Mathlib.Algebra.Order.Group.Bounds
- Banned modules (itself + downstream)
- 1
- Reference proof premises (reachable / held-out)
- 6 / 0
Traces
Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.
No configuration has attempted this theorem yet.
Reference proof
Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.
theorem IsLUB.exists_between_sub_self (h : IsLUB s a) (hε : 0 < ε) : ∃ b ∈ s, a - ε < b ∧ b ≤ a := h.exists_between <| sub_lt_self _ hε