internlm/Lean-Github huggingface dataset:
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : NeBot ℱ
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Tactic:
have hℱs : ℱ ≤ 𝓟 s :=
  iInf_le_of_le ⟨ne_s.choose, ne_s.choose_spec⟩ (principal_mono.mpr <| inter_subset_left _ _)
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Tactic:
have hℱ : ∀ x ∈ s, ∀ᶠ y in ℱ, f y ≤ f x := fun x hx =>
  mem_iInf_of_mem ⟨x, hx⟩ (by simp only [mem_principal]; apply inter_subset_right)
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Tactic:
obtain ⟨a, ha, h⟩ := hs hℱs
Proof state after:
case intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
case intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Tactic:
letI : (𝓝 a ⊓ ℱ).NeBot := h
Proof state after:
case intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝² : Nonempty α
this✝¹ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this✝ : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
this : NeBot (𝓝 a ⊓ ℱ) := h
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
case intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝² : Nonempty α
this✝¹ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this✝ : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
this : NeBot (𝓝 a ⊓ ℱ) := h
⊢ ∃ a ∈ s, ∀ x ∈ s, f a ≤ f x
Tactic:
refine' ⟨a, ha, fun x hx => le_of_not_lt fun hxa => _⟩
Proof state after:
case intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝² : Nonempty α
this✝¹ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this✝ : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
this : NeBot (𝓝 a ⊓ ℱ) := h
x : α
hx : x ∈ s
hxa : f x < f a
⊢ False
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
case intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝² : Nonempty α
this✝¹ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this✝ : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
this : NeBot (𝓝 a ⊓ ℱ) := h
x : α
hx : x ∈ s
hxa : f x < f a
⊢ False
Tactic:
suffices ∀ᶠ _ in 𝓝 a ⊓ ℱ, False by rwa [eventually_const] at this
Proof state after:
case intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝² : Nonempty α
this✝¹ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this✝ : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
this : NeBot (𝓝 a ⊓ ℱ) := h
x : α
hx : x ∈ s
hxa : f x < f a
⊢ ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
case intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝² : Nonempty α
this✝¹ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this✝ : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
this : NeBot (𝓝 a ⊓ ℱ) := h
x : α
hx : x ∈ s
hxa : f x < f a
⊢ ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False
Tactic:
filter_upwards [(hf a ha (f x) hxa).filter_mono (inf_le_inf_left _ hℱs),
  (hℱ x hx).filter_mono (inf_le_right : 𝓝 a ⊓ ℱ ≤ ℱ)] using fun y h₁ h₂ => not_le_of_lt h₁ h₂
Proof state after:
no goals
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ NeBot ℱ
Tactic:
refine' iInf_neBot_of_directed _ _
Proof state after:
case refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ Directed (fun x x_1 => x ≥ x_1) fun a => φ (f ↑a)

case refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ ∀ (i : ↑s), NeBot (φ (f ↑i))
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
case refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ Directed (fun x x_1 => x ≥ x_1) fun a => φ (f ↑a)
Tactic:
change Directed GE.ge (fun x ↦ (φ ∘ (fun (a : s) ↦ f ↑a)) x)
Proof state after:
case refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ Directed GE.ge fun x => (φ ∘ fun a => f ↑a) x
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
case refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ Directed GE.ge fun x => (φ ∘ fun a => f ↑a) x
Tactic:
refine' Directed.mono_comp GE.ge _ _
Proof state after:
case refine'_1.refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ ∀ ⦃x y : β⦄, x ≥ y → φ x ≥ φ y

case refine'_1.refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ Directed GE.ge fun a => f ↑a
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
case refine'_1.refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ ∀ ⦃x y : β⦄, x ≥ y → φ x ≥ φ y
Tactic:
intro x y hxy
Proof state after:
case refine'_1.refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
x y : β
hxy : x ≥ y
⊢ φ x ≥ φ y
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
case refine'_1.refine'_1
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
x y : β
hxy : x ≥ y
⊢ φ x ≥ φ y
Tactic:
refine'
  principal_mono.mpr (inter_subset_inter_right _ (preimage_mono <| Iic_subset_Iic.mpr hxy))
Proof state after:
no goals
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
case refine'_1.refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ Directed GE.ge fun a => f ↑a
Tactic:
apply IsTotal.directed' GE.ge
Proof state after:
no goals
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
case refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
⊢ ∀ (i : ↑s), NeBot (φ (f ↑i))
Tactic:
intro x
Proof state after:
case refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
x : ↑s
⊢ NeBot (φ (f ↑x))
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
case refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝ : Nonempty α
this : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
x : ↑s
⊢ NeBot (φ (f ↑x))
Tactic:
have : (pure x : Filter α) ≤ φ (f x) := le_principal_iff.mpr ⟨x.2, le_refl (f x)⟩
Proof state after:
case refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
x : ↑s
this : pure ↑x ≤ φ (f ↑x)
⊢ NeBot (φ (f ↑x))
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
case refine'_2
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
x : ↑s
this : pure ↑x ≤ φ (f ↑x)
⊢ NeBot (φ (f ↑x))
Tactic:
exact neBot_of_le this
Proof state after:
no goals
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
x : α
hx : x ∈ s
⊢ {x_1 | (fun y => f y ≤ f x) x_1} ∈ φ (f ↑{ val := x, property := hx })
Tactic:
simp only [mem_principal]
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
x : α
hx : x ∈ s
⊢ {x_1 | f x_1 ≤ f x} ∈ φ (f x)
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝¹ : Nonempty α
this✝ : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
x : α
hx : x ∈ s
⊢ {x_1 | f x_1 ≤ f x} ∈ φ (f x)
Tactic:
apply inter_subset_right
Proof state after:
no goals
Theorem: LowerSemicontinuousOn.exists_forall_le_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : LowerSemicontinuousOn f s
this✝³ : Nonempty α
this✝² : Nonempty ↑s
φ : β → Filter α := fun b => 𝓟 (s ∩ f ⁻¹' Iic b)
ℱ : Filter α := ⨅ a, φ (f ↑a)
this✝¹ : NeBot ℱ
hℱs : ℱ ≤ 𝓟 s
hℱ : ∀ x ∈ s, ∀ᶠ (y : α) in ℱ, f y ≤ f x
a : α
ha : a ∈ s
h : ClusterPt a ℱ
this✝ : NeBot (𝓝 a ⊓ ℱ) := h
x : α
hx : x ∈ s
hxa : f x < f a
this : ∀ᶠ (x : α) in 𝓝 a ⊓ ℱ, False
⊢ False
Tactic:
rwa [eventually_const] at this
Proof state after:
no goals
Theorem: LowerSemicontinuousOn.bddBelow_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
⊢ BddBelow (f '' s)
Tactic:
cases s.eq_empty_or_nonempty with
| inl h =>
    simp only [h, Set.image_empty]
    exact bddBelow_empty
| inr h =>
    obtain ⟨a, _, has⟩ := LowerSemicontinuousOn.exists_forall_le_of_isCompact h hs hf
    use f a
    rintro b ⟨x, hx, rfl⟩; exact has x hx
Proof state after:
no goals
Theorem: LowerSemicontinuousOn.bddBelow_of_isCompact
Proof state before:
case inl
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow (f '' s)
Tactic:
simp only [h, Set.image_empty]
Proof state after:
case inl
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow ∅
Theorem: LowerSemicontinuousOn.bddBelow_of_isCompact
Proof state before:
case inl
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : s = ∅
⊢ BddBelow ∅
Tactic:
exact bddBelow_empty
Proof state after:
no goals
Theorem: LowerSemicontinuousOn.bddBelow_of_isCompact
Proof state before:
case inr
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
⊢ BddBelow (f '' s)
Tactic:
obtain ⟨a, _, has⟩ := LowerSemicontinuousOn.exists_forall_le_of_isCompact h hs hf
Proof state after:
case inr.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
⊢ BddBelow (f '' s)
Theorem: LowerSemicontinuousOn.bddBelow_of_isCompact
Proof state before:
case inr.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
⊢ BddBelow (f '' s)
Tactic:
use f a
Proof state after:
case h
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
⊢ f a ∈ lowerBounds (f '' s)
Theorem: LowerSemicontinuousOn.bddBelow_of_isCompact
Proof state before:
case h
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
⊢ f a ∈ lowerBounds (f '' s)
Tactic:
rintro b ⟨x, hx, rfl⟩
Proof state after:
case h.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
x : α
hx : x ∈ s
⊢ f a ≤ f x
Theorem: LowerSemicontinuousOn.bddBelow_of_isCompact
Proof state before:
case h.intro.intro
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
f : α → β
inst✝² : LinearOrder β
inst✝¹ : OrderClosedTopology β
inst✝ : Nonempty β
s : Set α
hs : IsCompact s
hf : LowerSemicontinuousOn f s
h : Set.Nonempty s
a : α
left✝ : a ∈ s
has : ∀ x ∈ s, f a ≤ f x
x : α
hx : x ∈ s
⊢ f a ≤ f x
Tactic:
exact has x hx
Proof state after:
no goals
Theorem: UpperSemicontinuousOn.exists_forall_ge_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : UpperSemicontinuousOn f s
⊢ ∃ a ∈ s, ∀ x ∈ s, f x ≤ f a
Tactic:
apply LowerSemicontinuousOn.exists_forall_le_of_isCompact (β := βᵒᵈ) ne_s hs
Proof state after:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : UpperSemicontinuousOn f s
⊢ LowerSemicontinuousOn (fun x => f x) s
Theorem: UpperSemicontinuousOn.exists_forall_ge_of_isCompact
Proof state before:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
f : α → β
inst✝¹ : LinearOrder β
inst✝ : OrderClosedTopology β
s : Set α
ne_s : Set.Nonempty s
hs : IsCompact s
hf : UpperSemicontinuousOn f s
⊢ LowerSemicontinuousOn (fun x => f x) s
Tactic:
exact hf
Proof state after:
no goals
Theorem: LowerSemicontinuousOn.exists_iInf_of_isCompact
Proof state before:
β : 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 ∈ s, f a = ⨅ x ∈ s, f x
Tactic:
obtain ⟨a, ha, ha_le⟩ := LowerSemicontinuousOn.exists_forall_le_of_isCompact ne_s hs hf
Proof state after:
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