Theorem: lowerSemicontinuousWithinAt_supr₂ (Sion/Semicontinuous.lean)

State before:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
hf : ∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a
⊢ LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ I, f i x) s a
Tactic:
revert hf
State after:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
⊢ (∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ I, f i x) s a

State before:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
⊢ (∀ i ∈ I, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ I, f i x) s a
Tactic:
refine' Set.Finite.induction_on hI _ _
State after:
case refine'_1
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
⊢ (∀ i ∈ ∅, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ ∅, f i x) s a

case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
⊢ ∀ {a_1 : ι} {s_1 : Set ι},
    a_1 ∉ s_1 →
      Set.Finite s_1 →
        ((∀ i ∈ s_1, LowerSemicontinuousWithinAt (f i) s a) →
            LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ s_1, f i x) s a) →
          (∀ i ∈ insert a_1 s_1, LowerSemicontinuousWithinAt (f i) s a) →
            LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ insert a_1 s_1, f i x) s a

State before:
case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
⊢ ∀ {a_1 : ι} {s_1 : Set ι},
    a_1 ∉ s_1 →
      Set.Finite s_1 →
        ((∀ i ∈ s_1, LowerSemicontinuousWithinAt (f i) s a) →
            LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ s_1, f i x) s a) →
          (∀ i ∈ insert a_1 s_1, LowerSemicontinuousWithinAt (f i) s a) →
            LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ insert a_1 s_1, f i x) s a
Tactic:
intro j J _ _ hrec hf
State after:
case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
⊢ LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ insert j J, f i x) s a

State before:
case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
⊢ LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ insert j J, f i x) s a
Tactic:
suffices ∀ x, (⨆ (i : ι) (_ : i ∈ insert j J), f i x) = f j x ⊔ ⨆ i ∈ J, f i x by
  rw [funext this]
  apply LowerSemicontinuousWithinAt.sup (hf j (Set.mem_insert j J))
  apply hrec
  intro i hi; exact hf i (Set.mem_insert_of_mem j hi)
State after:
case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
⊢ ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x

State before:
case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
⊢ ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
Tactic:
intro x
State after:
case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
x : α
⊢ ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x

State before:
case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
x : α
⊢ ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
Tactic:
simp only [Set.insert_eq]
State after:
case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
x : α
⊢ ⨆ i ∈ {j} ∪ J, f i x = f j x ⊔ ⨆ i ∈ J, f i x

State before:
case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
x : α
⊢ ⨆ i ∈ {j} ∪ J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
Tactic:
rw [iSup_union]
State after:
case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
x : α
⊢ (⨆ x_1 ∈ {j}, f x_1 x) ⊔ ⨆ x_1 ∈ J, f x_1 x = f j x ⊔ ⨆ i ∈ J, f i x

State before:
case refine'_2
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
x : α
⊢ (⨆ x_1 ∈ {j}, f x_1 x) ⊔ ⨆ x_1 ∈ J, f x_1 x = f j x ⊔ ⨆ i ∈ J, f i x
Tactic:
apply congr_arg₂ _ _ rfl
State after:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
x : α
⊢ ⨆ x_1 ∈ {j}, f x_1 x = f j x

State before:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
x : α
⊢ ⨆ x_1 ∈ {j}, f x_1 x = f j x
Tactic:
simp only [mem_singleton_iff, iSup_iSup_eq_left]
State after:
no goals

State before:
case refine'_1
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
⊢ (∀ i ∈ ∅, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ ∅, f i x) s a
Tactic:
intro _
State after:
case refine'_1
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
hf✝ : ∀ i ∈ ∅, LowerSemicontinuousWithinAt (f i) s a
⊢ LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ ∅, f i x) s a

State before:
case refine'_1
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
hf✝ : ∀ i ∈ ∅, LowerSemicontinuousWithinAt (f i) s a
⊢ LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ ∅, f i x) s a
Tactic:
simp only [mem_empty_iff_false, ciSup_false, iSup_bot]
State after:
case refine'_1
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
hf✝ : ∀ i ∈ ∅, LowerSemicontinuousWithinAt (f i) s a
⊢ LowerSemicontinuousWithinAt (fun x => ⊥) s a

State before:
case refine'_1
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
hf✝ : ∀ i ∈ ∅, LowerSemicontinuousWithinAt (f i) s a
⊢ LowerSemicontinuousWithinAt (fun x => ⊥) s a
Tactic:
exact lowerSemicontinuousWithinAt_const
State after:
no goals

State before:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
this : ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
⊢ LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ insert j J, f i x) s a
Tactic:
rw [funext this]
State after:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
this : ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
⊢ LowerSemicontinuousWithinAt (fun x => f j x ⊔ ⨆ i ∈ J, f i x) s a

State before:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
this : ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
⊢ LowerSemicontinuousWithinAt (fun x => f j x ⊔ ⨆ i ∈ J, f i x) s a
Tactic:
apply LowerSemicontinuousWithinAt.sup (hf j (Set.mem_insert j J))
State after:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
this : ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
⊢ LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a

State before:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
this : ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
⊢ LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
Tactic:
apply hrec
State after:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
this : ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
⊢ ∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a

State before:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
this : ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
⊢ ∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a
Tactic:
intro i hi
State after:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
this : ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
i : ι
hi : i ∈ J
⊢ LowerSemicontinuousWithinAt (f i) s a

State before:
β : Type u_3
α : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f✝ : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
ι : Type u_1
f : ι → α → β
s : Set α
a : α
I : Set ι
hI : Set.Finite I
j : ι
J : Set ι
a✝¹ : j ∉ J
a✝ : Set.Finite J
hrec : (∀ i ∈ J, LowerSemicontinuousWithinAt (f i) s a) → LowerSemicontinuousWithinAt (fun x => ⨆ i ∈ J, f i x) s a
hf : ∀ i ∈ insert j J, LowerSemicontinuousWithinAt (f i) s a
this : ∀ (x : α), ⨆ i ∈ insert j J, f i x = f j x ⊔ ⨆ i ∈ J, f i x
i : ι
hi : i ∈ J
⊢ LowerSemicontinuousWithinAt (f i) s a
Tactic:
exact hf i (Set.mem_insert_of_mem j hi)
State after:
no goals