internlm/Lean-Github huggingface dataset:
Theorem: LowerSemicontinuousOn.exists_iInf_of_isCompact
Proof state before:
case intro.intro
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ∃ a ∈ s, f a = ⨅ x ∈ s, f x
Tactic:
use a
Proof state after:
case h
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ a ∈ s ∧ f a = ⨅ x ∈ s, f x
Theorem: LowerSemicontinuousOn.exists_iInf_of_isCompact
Proof state before:
case h
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ a ∈ s ∧ f a = ⨅ x ∈ s, f x
Tactic:
apply And.intro ha
Proof state after:
case h
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ f a = ⨅ x ∈ s, f x
Theorem: LowerSemicontinuousOn.exists_iInf_of_isCompact
Proof state before:
case h
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ f a = ⨅ x ∈ s, f x
Tactic:
apply le_antisymm
Proof state after:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ f a ≤ ⨅ x ∈ s, f x

case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a
Theorem: LowerSemicontinuousOn.exists_iInf_of_isCompact
Proof state before:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ f a ≤ ⨅ x ∈ s, f x

case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a
Tactic:
rw [le_iInf₂_iff]
Proof state after:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ∀ i ∈ s, f a ≤ f i

case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a
Theorem: LowerSemicontinuousOn.exists_iInf_of_isCompact
Proof state before:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ∀ i ∈ s, f a ≤ f i

case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a
Tactic:
intro x hx
Proof state after:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
x : α
hx : x ∈ s
⊢ f a ≤ f x

case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a
Theorem: LowerSemicontinuousOn.exists_iInf_of_isCompact
Proof state before:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
x : α
hx : x ∈ s
⊢ f a ≤ f x

case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a
Tactic:
exact ha_le x hx
Proof state after:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a
Theorem: LowerSemicontinuousOn.exists_iInf_of_isCompact
Proof state before:
case h.a
β : Type u_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : CompleteLinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
a : α
ha : a ∈ s
ha_le : ∀ x ∈ s, f a ≤ f x
⊢ ⨅ x ∈ s, f x ≤ f a
Tactic:
exact iInf₂_le a ha
Proof state after:
no goals
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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 _ _
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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)
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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]
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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]
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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]
Proof state after:
no goals
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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 _
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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]
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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
Proof state after:
no goals
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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]
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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))
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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
Proof 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
Theorem: lowerSemicontinuousWithinAt_supr₂
Proof 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
Proof 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