Theorem: ContinuousOn.partialSups (Ray/Misc/Max.lean)

State before:
A : Type
inst✝ : TopologicalSpace A
f : ℕ → A → ℝ
s : Set A
fc : ∀ (n : ℕ), ContinuousOn (f n) s
n : ℕ
⊢ ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n) s
Tactic:
induction' n with n h
State after:
case zero
A : Type
inst✝ : TopologicalSpace A
f : ℕ → A → ℝ
s : Set A
fc : ∀ (n : ℕ), ContinuousOn (f n) s
⊢ ContinuousOn (fun x => (_root_.partialSups fun k => f k x) 0) s

case succ
A : Type
inst✝ : TopologicalSpace A
f : ℕ → A → ℝ
s : Set A
fc : ∀ (n : ℕ), ContinuousOn (f n) s
n : ℕ
h : ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n) s
⊢ ContinuousOn (fun x => (_root_.partialSups fun k => f k x) (n + 1)) s

State before:
case zero
A : Type
inst✝ : TopologicalSpace A
f : ℕ → A → ℝ
s : Set A
fc : ∀ (n : ℕ), ContinuousOn (f n) s
⊢ ContinuousOn (fun x => (_root_.partialSups fun k => f k x) 0) s

case succ
A : Type
inst✝ : TopologicalSpace A
f : ℕ → A → ℝ
s : Set A
fc : ∀ (n : ℕ), ContinuousOn (f n) s
n : ℕ
h : ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n) s
⊢ ContinuousOn (fun x => (_root_.partialSups fun k => f k x) (n + 1)) s
Tactic:
simp [fc 0]
State after:
case succ
A : Type
inst✝ : TopologicalSpace A
f : ℕ → A → ℝ
s : Set A
fc : ∀ (n : ℕ), ContinuousOn (f n) s
n : ℕ
h : ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n) s
⊢ ContinuousOn (fun x => (_root_.partialSups fun k => f k x) (n + 1)) s

State before:
case succ
A : Type
inst✝ : TopologicalSpace A
f : ℕ → A → ℝ
s : Set A
fc : ∀ (n : ℕ), ContinuousOn (f n) s
n : ℕ
h : ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n) s
⊢ ContinuousOn (fun x => (_root_.partialSups fun k => f k x) (n + 1)) s
Tactic:
simp
State after:
case succ
A : Type
inst✝ : TopologicalSpace A
f : ℕ → A → ℝ
s : Set A
fc : ∀ (n : ℕ), ContinuousOn (f n) s
n : ℕ
h : ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n) s
⊢ ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n ⊔ f (n + 1) x) s

State before:
case succ
A : Type
inst✝ : TopologicalSpace A
f : ℕ → A → ℝ
s : Set A
fc : ∀ (n : ℕ), ContinuousOn (f n) s
n : ℕ
h : ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n) s
⊢ ContinuousOn (fun x => (_root_.partialSups fun k => f k x) n ⊔ f (n + 1) x) s
Tactic:
exact ContinuousOn.max h (fc _)
State after:
no goals