Theorem: convexOn_max (Ray/Misc/Max.lean)

State before:
⊢ ConvexOn ℝ univ fun p => max p.1 p.2
Tactic:
apply ConvexOn.sup
State after:
case hf

⊢ ConvexOn ℝ univ fun p => p.1

case hg

⊢ ConvexOn ℝ univ fun p => p.2

State before:
case hf

⊢ ConvexOn ℝ univ fun p => p.1
Tactic:
use convex_univ
State after:
case right

⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ univ → ∀ ⦃y : ℝ × ℝ⦄, y ∈ univ → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y).1 ≤ a • x.1 + b • y.1

State before:
case right

⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ univ → ∀ ⦃y : ℝ × ℝ⦄, y ∈ univ → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y).1 ≤ a • x.1 + b • y.1
Tactic:
intros
State after:
case right
x✝ : ℝ × ℝ
a✝⁵ : x✝ ∈ univ
y✝ : ℝ × ℝ
a✝⁴ : y✝ ∈ univ
a✝³ b✝ : ℝ
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ (a✝³ • x✝ + b✝ • y✝).1 ≤ a✝³ • x✝.1 + b✝ • y✝.1

State before:
case right
x✝ : ℝ × ℝ
a✝⁵ : x✝ ∈ univ
y✝ : ℝ × ℝ
a✝⁴ : y✝ ∈ univ
a✝³ b✝ : ℝ
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ (a✝³ • x✝ + b✝ • y✝).1 ≤ a✝³ • x✝.1 + b✝ • y✝.1
Tactic:
simp
State after:
no goals

State before:
case hg

⊢ ConvexOn ℝ univ fun p => p.2
Tactic:
use convex_univ
State after:
case right

⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ univ → ∀ ⦃y : ℝ × ℝ⦄, y ∈ univ → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y).2 ≤ a • x.2 + b • y.2

State before:
case right

⊢ ∀ ⦃x : ℝ × ℝ⦄,
    x ∈ univ → ∀ ⦃y : ℝ × ℝ⦄, y ∈ univ → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → (a • x + b • y).2 ≤ a • x.2 + b • y.2
Tactic:
intros
State after:
case right
x✝ : ℝ × ℝ
a✝⁵ : x✝ ∈ univ
y✝ : ℝ × ℝ
a✝⁴ : y✝ ∈ univ
a✝³ b✝ : ℝ
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ (a✝³ • x✝ + b✝ • y✝).2 ≤ a✝³ • x✝.2 + b✝ • y✝.2

State before:
case right
x✝ : ℝ × ℝ
a✝⁵ : x✝ ∈ univ
y✝ : ℝ × ℝ
a✝⁴ : y✝ ∈ univ
a✝³ b✝ : ℝ
a✝² : 0 ≤ a✝³
a✝¹ : 0 ≤ b✝
a✝ : a✝³ + b✝ = 1
⊢ (a✝³ • x✝ + b✝ • y✝).2 ≤ a✝³ • x✝.2 + b✝ • y✝.2
Tactic:
simp
State after:
no goals