def G67SumCoordinate.lower (a d s : ℝ) : ℝ

Lower endpoint of the sum-coordinate fiber.

Equations

• G67SumCoordinate.lower a d s = max a (s - d)

def G67SumCoordinate.upper (b c s : ℝ) : ℝ

Upper endpoint of the sum-coordinate fiber.

Equations

• G67SumCoordinate.upper b c s = min b (s - c)

theorem G67SumCoordinate.fiber_bounds {a b c d s : ℝ} (ha : 0 < a) (hc : 0 < c) (hab : a ≤ b) (hcd : c ≤ d) (hs : s ∈ Set.Icc (a + c) (b + d)) : 0 < lower a d s ∧ lower a d s ≤ upper b c s ∧ 0 < s - upper b c s

The fiber is a nonempty positive interval throughout the sum range.

theorem G67SumCoordinate.fiber_mem {a b c d s u : ℝ} : u ∈ Set.Icc (lower a d s) (upper b c s) ↔ u ∈ Set.Icc a b ∧ s - u ∈ Set.Icc c d

Exact closed-domain equivalence; no coordinate substitution is assumed.