[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
⊢ IsCompact (Icc a b)
[PROOFSTEP]
rw [Icc_eq_empty hab]
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : Preorder α
h : ∀ {a b : α}, a ≤ b → IsCompact (Icc a b)
a b : α
hab : ¬a ≤ b
⊢ IsCompact ∅
[PROOFSTEP]
exact isCompact_empty
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PartialOrder α
h : ∀ {a b : α}, a < b → IsCompact (Icc a b)
a✝ b✝ : α
hab : a✝ ≤ b✝
⊢ a✝ = b✝ → IsCompact (Icc a✝ b✝)
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : PartialOrder α
h : ∀ {a b : α}, a < b → IsCompact (Icc a b)
a✝ : α
hab : a✝ ≤ a✝
⊢ IsCompact (Icc a✝ a✝)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ CompactIccSpace α
[PROOFSTEP]
refine' .mk'' fun {a b} hlt => ?_
[GOAL]
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
⊢ IsCompact (Icc a b)
[PROOFSTEP]
cases' le_or_lt a b with hab hab
[GOAL]
case inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
⊢ IsCompact (Icc a b)
case inr
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : b < a
⊢ IsCompact (Icc a b)
[PROOFSTEP]
swap
[GOAL]
case inr
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : b < a
⊢ IsCompact (Icc a b)
[PROOFSTEP]
simp [hab]
[GOAL]
case inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
⊢ IsCompact (Icc a b)
[PROOFSTEP]
refine' isCompact_iff_ultrafilter_le_nhds.2 fun f hf => _
[GOAL]
case inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hf : ↑f ≤ 𝓟 (Icc a b)
⊢ ∃ a_1, a_1 ∈ Icc a b ∧ ↑f ≤ 𝓝 a_1
[PROOFSTEP]
contrapose! hf
[GOAL]
case inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hf : ∀ (a_1 : α), a_1 ∈ Icc a b → ¬↑f ≤ 𝓝 a_1
⊢ ¬↑f ≤ 𝓟 (Icc a b)
[PROOFSTEP]
rw [le_principal_iff]
[GOAL]
case inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hf : ∀ (a_1 : α), a_1 ∈ Icc a b → ¬↑f ≤ 𝓝 a_1
⊢ ¬Icc a b ∈ ↑f
[PROOFSTEP]
have hpt : ∀ x ∈ Icc a b, { x } ∉ f := fun x hx hxf => hf x hx ((le_pure_iff.2 hxf).trans (pure_le_nhds x))
[GOAL]
case inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hf : ∀ (a_1 : α), a_1 ∈ Icc a b → ¬↑f ≤ 𝓝 a_1
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
⊢ ¬Icc a b ∈ ↑f
[PROOFSTEP]
set s := {x ∈ Icc a b | Icc a x ∉ f}
[GOAL]
case inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hf : ∀ (a_1 : α), a_1 ∈ Icc a b → ¬↑f ≤ 𝓝 a_1
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
⊢ ¬Icc a b ∈ ↑f
[PROOFSTEP]
have hsb : b ∈ upperBounds s := fun x hx => hx.1.2
[GOAL]
case inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hf : ∀ (a_1 : α), a_1 ∈ Icc a b → ¬↑f ≤ 𝓝 a_1
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
⊢ ¬Icc a b ∈ ↑f
[PROOFSTEP]
have sbd : BddAbove s := ⟨b, hsb⟩
[GOAL]
case inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hf : ∀ (a_1 : α), a_1 ∈ Icc a b → ¬↑f ≤ 𝓝 a_1
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
⊢ ¬Icc a b ∈ ↑f
[PROOFSTEP]
have ha : a ∈ s := by simp [hpt, hab]
[GOAL]
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hf : ∀ (a_1 : α), a_1 ∈ Icc a b → ¬↑f ≤ 𝓝 a_1
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
⊢ a ∈ s
[PROOFSTEP]
simp [hpt, hab]
[GOAL]
case inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hf : ∀ (a_1 : α), a_1 ∈ Icc a b → ¬↑f ≤ 𝓝 a_1
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
⊢ ¬Icc a b ∈ ↑f
[PROOFSTEP]
rcases hab.eq_or_lt with (rfl | _hlt)
[GOAL]
case inl.inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
f : Ultrafilter α
hlt : a < a
hab : a ≤ a
hf : ∀ (a_1 : α), a_1 ∈ Icc a a → ¬↑f ≤ 𝓝 a_1
hpt : ∀ (x : α), x ∈ Icc a a → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a a ∧ ¬Icc a x ∈ f}
hsb : a ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
⊢ ¬Icc a a ∈ ↑f
[PROOFSTEP]
exact
  ha.2
    -- porting note: the `obtain` below was instead
      -- `set c := Sup s`
      -- `have hsc : IsLUB s c := isLUB_csSup ⟨a, ha⟩ sbd`
[GOAL]
case inl.inr
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hf : ∀ (a_1 : α), a_1 ∈ Icc a b → ¬↑f ≤ 𝓝 a_1
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
⊢ ¬Icc a b ∈ ↑f
[PROOFSTEP]
obtain ⟨c, hsc⟩ : ∃ c, IsLUB s c := ⟨sSup s, isLUB_csSup ⟨a, ha⟩ ⟨b, hsb⟩⟩
[GOAL]
case inl.inr.intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hf : ∀ (a_1 : α), a_1 ∈ Icc a b → ¬↑f ≤ 𝓝 a_1
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
⊢ ¬Icc a b ∈ ↑f
[PROOFSTEP]
have hc : c ∈ Icc a b := ⟨hsc.1 ha, hsc.2 hsb⟩
[GOAL]
case inl.inr.intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hf : ∀ (a_1 : α), a_1 ∈ Icc a b → ¬↑f ≤ 𝓝 a_1
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
⊢ ¬Icc a b ∈ ↑f
[PROOFSTEP]
specialize hf c hc
[GOAL]
case inl.inr.intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hf : ¬↑f ≤ 𝓝 c
⊢ ¬Icc a b ∈ ↑f
[PROOFSTEP]
have hcs : c ∈ s := by
  rcases hc.1.eq_or_lt with (rfl | hlt); · assumption
  refine' ⟨hc, fun hcf => hf fun U hU => _⟩
  rcases(mem_nhdsWithin_Iic_iff_exists_Ioc_subset' hlt).1 (mem_nhdsWithin_of_mem_nhds hU) with ⟨x, hxc, hxU⟩
  rcases((hsc.frequently_mem ⟨a, ha⟩).and_eventually (Ioc_mem_nhdsWithin_Iic ⟨hxc, le_rfl⟩)).exists with
    ⟨y, ⟨_hyab, hyf⟩, hy⟩
  refine' mem_of_superset (f.diff_mem_iff.2 ⟨hcf, hyf⟩) (Subset.trans _ hxU)
  rw [diff_subset_iff]
  exact Subset.trans Icc_subset_Icc_union_Ioc <| union_subset_union Subset.rfl <| Ioc_subset_Ioc_left hy.1.le
[GOAL]
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hf : ¬↑f ≤ 𝓝 c
⊢ c ∈ s
[PROOFSTEP]
rcases hc.1.eq_or_lt with (rfl | hlt)
[GOAL]
case inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
hsc : IsLUB s a
hc : a ∈ Icc a b
hf : ¬↑f ≤ 𝓝 a
⊢ a ∈ s
[PROOFSTEP]
assumption
[GOAL]
case inr
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hf : ¬↑f ≤ 𝓝 c
hlt : a < c
⊢ c ∈ s
[PROOFSTEP]
refine' ⟨hc, fun hcf => hf fun U hU => _⟩
[GOAL]
case inr
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hf : ¬↑f ≤ 𝓝 c
hlt : a < c
hcf : Icc a c ∈ f
U : Set α
hU : U ∈ 𝓝 c
⊢ U ∈ ↑f
[PROOFSTEP]
rcases(mem_nhdsWithin_Iic_iff_exists_Ioc_subset' hlt).1 (mem_nhdsWithin_of_mem_nhds hU) with ⟨x, hxc, hxU⟩
[GOAL]
case inr.intro.intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hf : ¬↑f ≤ 𝓝 c
hlt : a < c
hcf : Icc a c ∈ f
U : Set α
hU : U ∈ 𝓝 c
x : α
hxc : x ∈ Iio c
hxU : Ioc x c ⊆ U
⊢ U ∈ ↑f
[PROOFSTEP]
rcases((hsc.frequently_mem ⟨a, ha⟩).and_eventually (Ioc_mem_nhdsWithin_Iic ⟨hxc, le_rfl⟩)).exists with
  ⟨y, ⟨_hyab, hyf⟩, hy⟩
[GOAL]
case inr.intro.intro.intro.intro.intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hf : ¬↑f ≤ 𝓝 c
hlt : a < c
hcf : Icc a c ∈ f
U : Set α
hU : U ∈ 𝓝 c
x : α
hxc : x ∈ Iio c
hxU : Ioc x c ⊆ U
y : α
hy : x < y ∧ y ≤ c
_hyab : y ∈ Icc a b
hyf : ¬Icc a y ∈ f
⊢ U ∈ ↑f
[PROOFSTEP]
refine' mem_of_superset (f.diff_mem_iff.2 ⟨hcf, hyf⟩) (Subset.trans _ hxU)
[GOAL]
case inr.intro.intro.intro.intro.intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hf : ¬↑f ≤ 𝓝 c
hlt : a < c
hcf : Icc a c ∈ f
U : Set α
hU : U ∈ 𝓝 c
x : α
hxc : x ∈ Iio c
hxU : Ioc x c ⊆ U
y : α
hy : x < y ∧ y ≤ c
_hyab : y ∈ Icc a b
hyf : ¬Icc a y ∈ f
⊢ Icc a c \ Icc a y ⊆ Ioc x c
[PROOFSTEP]
rw [diff_subset_iff]
[GOAL]
case inr.intro.intro.intro.intro.intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hf : ¬↑f ≤ 𝓝 c
hlt : a < c
hcf : Icc a c ∈ f
U : Set α
hU : U ∈ 𝓝 c
x : α
hxc : x ∈ Iio c
hxU : Ioc x c ⊆ U
y : α
hy : x < y ∧ y ≤ c
_hyab : y ∈ Icc a b
hyf : ¬Icc a y ∈ f
⊢ Icc a c ⊆ Icc a y ∪ Ioc x c
[PROOFSTEP]
exact Subset.trans Icc_subset_Icc_union_Ioc <| union_subset_union Subset.rfl <| Ioc_subset_Ioc_left hy.1.le
[GOAL]
case inl.inr.intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hf : ¬↑f ≤ 𝓝 c
hcs : c ∈ s
⊢ ¬Icc a b ∈ ↑f
[PROOFSTEP]
rcases hc.2.eq_or_lt with (rfl | hlt)
[GOAL]
case inl.inr.intro.inl
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a : α
f : Ultrafilter α
c : α
hf : ¬↑f ≤ 𝓝 c
hlt : a < c
hab : a ≤ c
hpt : ∀ (x : α), x ∈ Icc a c → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a c ∧ ¬Icc a x ∈ f}
hsb : c ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < c
hsc : IsLUB s c
hc : c ∈ Icc a c
hcs : c ∈ s
⊢ ¬Icc a c ∈ ↑f
[PROOFSTEP]
exact hcs.2
[GOAL]
case inl.inr.intro.inr
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hf : ¬↑f ≤ 𝓝 c
hcs : c ∈ s
hlt : c < b
⊢ ¬Icc a b ∈ ↑f
[PROOFSTEP]
contrapose! hf
[GOAL]
case inl.inr.intro.inr
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hcs : c ∈ s
hlt : c < b
hf : Icc a b ∈ ↑f
⊢ ↑f ≤ 𝓝 c
[PROOFSTEP]
intro U hU
[GOAL]
case inl.inr.intro.inr
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hcs : c ∈ s
hlt : c < b
hf : Icc a b ∈ ↑f
U : Set α
hU : U ∈ 𝓝 c
⊢ U ∈ ↑f
[PROOFSTEP]
rcases(mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset hlt).1 (mem_nhdsWithin_of_mem_nhds hU) with ⟨y, hxy, hyU⟩
[GOAL]
case inl.inr.intro.inr.intro.intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hcs : c ∈ s
hlt : c < b
hf : Icc a b ∈ ↑f
U : Set α
hU : U ∈ 𝓝 c
y : α
hxy : y ∈ Ioc c b
hyU : Ico c y ⊆ U
⊢ U ∈ ↑f
[PROOFSTEP]
refine' mem_of_superset _ hyU
[GOAL]
case inl.inr.intro.inr.intro.intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hcs : c ∈ s
hlt : c < b
hf : Icc a b ∈ ↑f
U : Set α
hU : U ∈ 𝓝 c
y : α
hxy : y ∈ Ioc c b
hyU : Ico c y ⊆ U
⊢ Ico c y ∈ ↑f
[PROOFSTEP]
clear! U
[GOAL]
case inl.inr.intro.inr.intro.intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hcs : c ∈ s
hlt : c < b
hf : Icc a b ∈ ↑f
y : α
hxy : y ∈ Ioc c b
⊢ Ico c y ∈ ↑f
[PROOFSTEP]
have hy : y ∈ Icc a b := ⟨hc.1.trans hxy.1.le, hxy.2⟩
[GOAL]
case inl.inr.intro.inr.intro.intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hcs : c ∈ s
hlt : c < b
hf : Icc a b ∈ ↑f
y : α
hxy : y ∈ Ioc c b
hy : y ∈ Icc a b
⊢ Ico c y ∈ ↑f
[PROOFSTEP]
by_cases hay : Icc a y ∈ f
[GOAL]
case pos
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hcs : c ∈ s
hlt : c < b
hf : Icc a b ∈ ↑f
y : α
hxy : y ∈ Ioc c b
hy : y ∈ Icc a b
hay : Icc a y ∈ f
⊢ Ico c y ∈ ↑f
[PROOFSTEP]
refine' mem_of_superset (f.diff_mem_iff.2 ⟨f.diff_mem_iff.2 ⟨hay, hcs.2⟩, hpt y hy⟩) _
[GOAL]
case pos
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hcs : c ∈ s
hlt : c < b
hf : Icc a b ∈ ↑f
y : α
hxy : y ∈ Ioc c b
hy : y ∈ Icc a b
hay : Icc a y ∈ f
⊢ (Icc a y \ Icc a c) \ {y} ⊆ Ico c y
[PROOFSTEP]
rw [diff_subset_iff, union_comm, Ico_union_right hxy.1.le, diff_subset_iff]
[GOAL]
case pos
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hcs : c ∈ s
hlt : c < b
hf : Icc a b ∈ ↑f
y : α
hxy : y ∈ Ioc c b
hy : y ∈ Icc a b
hay : Icc a y ∈ f
⊢ Icc a y ⊆ Icc a c ∪ Icc c y
[PROOFSTEP]
exact Icc_subset_Icc_union_Icc
[GOAL]
case neg
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
a b : α
hlt✝ : a < b
hab : a ≤ b
f : Ultrafilter α
hpt : ∀ (x : α), x ∈ Icc a b → ¬{x} ∈ f
s : Set α := {x | x ∈ Icc a b ∧ ¬Icc a x ∈ f}
hsb : b ∈ upperBounds s
sbd : BddAbove s
ha : a ∈ s
_hlt : a < b
c : α
hsc : IsLUB s c
hc : c ∈ Icc a b
hcs : c ∈ s
hlt : c < b
hf : Icc a b ∈ ↑f
y : α
hxy : y ∈ Ioc c b
hy : y ∈ Icc a b
hay : ¬Icc a y ∈ f
⊢ Ico c y ∈ ↑f
[PROOFSTEP]
exact ((hsc.1 ⟨hy, hay⟩).not_lt hxy.1).elim
[GOAL]
α : Type u_1
inst✝² : CompleteLinearOrder α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ IsCompact univ
[PROOFSTEP]
simp only [← Icc_bot_top, isCompact_Icc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : Set.Nonempty s
⊢ ∃ x, IsLeast s x
[PROOFSTEP]
haveI : Nonempty s := ne_s.to_subtype
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : Set.Nonempty s
this : Nonempty ↑s
⊢ ∃ x, IsLeast s x
[PROOFSTEP]
suffices : (s ∩ ⋂ x ∈ s, Iic x).Nonempty
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : Set.Nonempty s
this✝ : Nonempty ↑s
this : Set.Nonempty (s ∩ ⋂ (x : α) (_ : x ∈ s), Iic x)
⊢ ∃ x, IsLeast s x
[PROOFSTEP]
exact ⟨this.choose, this.choose_spec.1, mem_iInter₂.mp this.choose_spec.2⟩
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : Set.Nonempty s
this : Nonempty ↑s
⊢ Set.Nonempty (s ∩ ⋂ (x : α) (_ : x ∈ s), Iic x)
[PROOFSTEP]
rw [biInter_eq_iInter]
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : Set.Nonempty s
this : Nonempty ↑s
⊢ Set.Nonempty (s ∩ ⋂ (x : ↑s), Iic ↑x)
[PROOFSTEP]
by_contra H
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : Set.Nonempty s
this : Nonempty ↑s
H : ¬Set.Nonempty (s ∩ ⋂ (x : ↑s), Iic ↑x)
⊢ False
[PROOFSTEP]
rw [not_nonempty_iff_eq_empty] at H
[GOAL]
case this
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : Set.Nonempty s
this : Nonempty ↑s
H : s ∩ ⋂ (x : ↑s), Iic ↑x = ∅
⊢ False
[PROOFSTEP]
rcases hs.elim_directed_family_closed (fun x : s => Iic ↑x) (fun x => isClosed_Iic) H
    (directed_of_inf fun _ _ h => Iic_subset_Iic.mpr h) with
  ⟨x, hx⟩
[GOAL]
case this.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set α
hs : IsCompact s
ne_s : Set.Nonempty s
this : Nonempty ↑s
H : s ∩ ⋂ (x : ↑s), Iic ↑x = ∅
x : ↑s
hx : s ∩ Iic ↑x = ∅
⊢ False
[PROOFSTEP]
exact not_nonempty_iff_eq_empty.mpr hx ⟨x, x.2, le_rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : Set.Nonempty s
f : β → α
hf : ContinuousOn f s
⊢ ∃ x, x ∈ s ∧ IsMinOn f s x
[PROOFSTEP]
rcases(hs.image_of_continuousOn hf).exists_isLeast (ne_s.image f) with ⟨_, ⟨x, hxs, rfl⟩, hx⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set β
hs : IsCompact s
ne_s : Set.Nonempty s
f : β → α
hf : ContinuousOn f s
x : β
hxs : x ∈ s
hx : f x ∈ lowerBounds (f '' s)
⊢ ∃ x, x ∈ s ∧ IsMinOn f s x
[PROOFSTEP]
exact ⟨x, hxs, ball_image_iff.1 hx⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
⊢ ∃ x, x ∈ s ∧ IsMinOn f s x
[PROOFSTEP]
rcases(hasBasis_cocompact.inf_principal _).eventually_iff.1 hc with ⟨K, hK, hKf⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
⊢ ∃ x, x ∈ s ∧ IsMinOn f s x
[PROOFSTEP]
have hsub : insert x₀ (K ∩ s) ⊆ s := insert_subset_iff.2 ⟨h₀, inter_subset_right _ _⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
⊢ ∃ x, x ∈ s ∧ IsMinOn f s x
[PROOFSTEP]
obtain ⟨x, hx, hxf⟩ : ∃ x ∈ insert x₀ (K ∩ s), ∀ y ∈ insert x₀ (K ∩ s), f x ≤ f y :=
  ((hK.inter_right hsc).insert x₀).exists_forall_le (insert_nonempty _ _) (hf.mono hsub)
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ (y : β), y ∈ insert x₀ (K ∩ s) → f x ≤ f y
⊢ ∃ x, x ∈ s ∧ IsMinOn f s x
[PROOFSTEP]
refine' ⟨x, hsub hx, fun y hy => _⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ (y : β), y ∈ insert x₀ (K ∩ s) → f x ≤ f y
y : β
hy : y ∈ s
⊢ y ∈ {x_1 | (fun x_2 => f x ≤ f x_2) x_1}
[PROOFSTEP]
by_cases hyK : y ∈ K
[GOAL]
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ (y : β), y ∈ insert x₀ (K ∩ s) → f x ≤ f y
y : β
hy : y ∈ s
hyK : y ∈ K
⊢ y ∈ {x_1 | (fun x_2 => f x ≤ f x_2) x_1}
case neg
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
s : Set β
f : β → α
hf : ContinuousOn f s
hsc : IsClosed s
x₀ : β
h₀ : x₀ ∈ s
hc : ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 s, f x₀ ≤ f x
K : Set β
hK : IsCompact K
hKf : ∀ ⦃x : β⦄, x ∈ Kᶜ ∩ s → f x₀ ≤ f x
hsub : insert x₀ (K ∩ s) ⊆ s
x : β
hx : x ∈ insert x₀ (K ∩ s)
hxf : ∀ (y : β), y ∈ insert x₀ (K ∩ s) → f x ≤ f y
y : β
hy : y ∈ s
hyK : ¬y ∈ K
⊢ y ∈ {x_1 | (fun x_2 => f x ≤ f x_2) x_1}
[PROOFSTEP]
exacts [hxf _ (Or.inr ⟨hyK, hy⟩), (hxf _ (Or.inl rfl)).trans (hKf ⟨hyK, hy⟩)]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIicTopology α
f : β → α
hf : Continuous f
x₀ : β
h : ∀ᶠ (x : β) in cocompact β, f x₀ ≤ f x
⊢ ∀ᶠ (x : β) in cocompact β ⊓ 𝓟 univ, f x₀ ≤ f x
[PROOFSTEP]
rwa [principal_univ, inf_top_eq]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty β
f : β → α
hf : Continuous f
hlim : Tendsto f (cocompact β) atTop
⊢ ∃ x, ∀ (y : β), f x ≤ f y
[PROOFSTEP]
inhabit β
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty β
f : β → α
hf : Continuous f
hlim : Tendsto f (cocompact β) atTop
inhabited_h : Inhabited β
⊢ ∃ x, ∀ (y : β), f x ≤ f y
[PROOFSTEP]
exact hf.exists_forall_le' default (hlim.eventually <| eventually_ge_atTop _)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous f
h : HasCompactMulSupport f
⊢ ∃ x, ∀ (y : β), f x ≤ f y
[PROOFSTEP]
obtain ⟨_, ⟨x, rfl⟩, hx⟩ := (h.isCompact_range hf).exists_isLeast (range_nonempty _)
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous f
h : HasCompactMulSupport f
x : β
hx : f x ∈ lowerBounds (range f)
⊢ ∃ x, ∀ (y : β), f x ≤ f y
[PROOFSTEP]
rw [mem_lowerBounds, forall_range_iff] at hx
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : ClosedIicTopology α
inst✝¹ : Nonempty β
inst✝ : One α
f : β → α
hf : Continuous f
h : HasCompactMulSupport f
x : β
hx : ∀ (i : β), f x ≤ f i
⊢ ∃ x, ∀ (y : β), f x ≤ f y
[PROOFSTEP]
exact ⟨x, hx⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
⊢ BddBelow s
[PROOFSTEP]
rcases s.eq_empty_or_nonempty with rfl | hne
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
hs : IsCompact ∅
⊢ BddBelow ∅
[PROOFSTEP]
exact bddBelow_empty
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : Set.Nonempty s
⊢ BddBelow s
[PROOFSTEP]
obtain ⟨a, -, has⟩ := hs.exists_isLeast hne
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
inst✝¹ : ClosedIicTopology α
inst✝ : Nonempty α
s : Set α
hs : IsCompact s
hne : Set.Nonempty s
a : α
has : a ∈ lowerBounds s
⊢ BddBelow s
[PROOFSTEP]
exact ⟨a, has⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : Set.Nonempty K
hf : ContinuousOn f K
y : α
⊢ sSup (f '' K) < y ↔ ∀ (x : β), x ∈ K → f x < y
[PROOFSTEP]
refine' ⟨fun h x hx => (le_csSup (hK.bddAbove_image hf) <| mem_image_of_mem f hx).trans_lt h, fun h => _⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : Set.Nonempty K
hf : ContinuousOn f K
y : α
h : ∀ (x : β), x ∈ K → f x < y
⊢ sSup (f '' K) < y
[PROOFSTEP]
obtain ⟨x, hx, h2x⟩ := hK.exists_forall_ge h0K hf
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : Set.Nonempty K
hf : ContinuousOn f K
y : α
h : ∀ (x : β), x ∈ K → f x < y
x : β
hx : x ∈ K
h2x : ∀ (y : β), y ∈ K → f y ≤ f x
⊢ sSup (f '' K) < y
[PROOFSTEP]
refine' (csSup_le (h0K.image f) _).trans_lt (h x hx)
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : Set.Nonempty K
hf : ContinuousOn f K
y : α
h : ∀ (x : β), x ∈ K → f x < y
x : β
hx : x ∈ K
h2x : ∀ (y : β), y ∈ K → f y ≤ f x
⊢ ∀ (b : α), b ∈ f '' K → b ≤ f x
[PROOFSTEP]
rintro _ ⟨x', hx', rfl⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : ClosedIciTopology α
f : β → α
K : Set β
hK : IsCompact K
h0K : Set.Nonempty K
hf : ContinuousOn f K
y : α
h : ∀ (x : β), x ∈ K → f x < y
x : β
hx : x ∈ K
h2x : ∀ (y : β), y ∈ K → f y ≤ f x
x' : β
hx' : x' ∈ K
⊢ f x' ≤ f x
[PROOFSTEP]
exact h2x x' hx'
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
⊢ Continuous fun x => sSup (f x '' K)
[PROOFSTEP]
rcases eq_empty_or_nonempty K with (rfl | h0K)
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
hf : Continuous ↿f
hK : IsCompact ∅
⊢ Continuous fun x => sSup (f x '' ∅)
[PROOFSTEP]
simp_rw [image_empty]
[GOAL]
case inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
hf : Continuous ↿f
hK : IsCompact ∅
⊢ Continuous fun x => sSup ∅
[PROOFSTEP]
exact continuous_const
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
⊢ Continuous fun x => sSup (f x '' K)
[PROOFSTEP]
rw [continuous_iff_continuousAt]
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
⊢ ∀ (x : γ), ContinuousAt (fun x => sSup (f x '' K)) x
[PROOFSTEP]
intro x
[GOAL]
case inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
x : γ
⊢ ContinuousAt (fun x => sSup (f x '' K)) x
[PROOFSTEP]
obtain ⟨y, hyK, h2y, hy⟩ :=
  hK.exists_sSup_image_eq_and_ge h0K (show Continuous fun y => f x y from hf.comp <| Continuous.Prod.mk x).continuousOn
[GOAL]
case inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ (y_1 : β), y_1 ∈ K → f x y_1 ≤ f x y
⊢ ContinuousAt (fun x => sSup (f x '' K)) x
[PROOFSTEP]
rw [ContinuousAt, h2y, tendsto_order]
[GOAL]
case inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ (y_1 : β), y_1 ∈ K → f x y_1 ≤ f x y
⊢ (∀ (a' : α), a' < f x y → ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧
    ∀ (a' : α), a' > f x y → ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'
[PROOFSTEP]
have :=
  tendsto_order.mp ((show Continuous fun x => f x y from hf.comp <| continuous_id.prod_mk continuous_const).tendsto x)
[GOAL]
case inr.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ (y_1 : β), y_1 ∈ K → f x y_1 ≤ f x y
this : (∀ (a' : α), a' < f x y → ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ (a' : α), a' > f x y → ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
⊢ (∀ (a' : α), a' < f x y → ∀ᶠ (b : γ) in 𝓝 x, a' < sSup (f b '' K)) ∧
    ∀ (a' : α), a' > f x y → ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < a'
[PROOFSTEP]
refine' ⟨fun z hz => _, fun z hz => _⟩
[GOAL]
case inr.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ (y_1 : β), y_1 ∈ K → f x y_1 ≤ f x y
this : (∀ (a' : α), a' < f x y → ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ (a' : α), a' > f x y → ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z < f x y
⊢ ∀ᶠ (b : γ) in 𝓝 x, z < sSup (f b '' K)
[PROOFSTEP]
refine' (this.1 z hz).mono fun x' hx' => hx'.trans_le <| le_csSup _ <| mem_image_of_mem (f x') hyK
[GOAL]
case inr.intro.intro.intro.refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ (y_1 : β), y_1 ∈ K → f x y_1 ≤ f x y
this : (∀ (a' : α), a' < f x y → ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ (a' : α), a' > f x y → ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z < f x y
x' : γ
hx' : z < f x' y
⊢ BddAbove (f x' '' K)
[PROOFSTEP]
exact hK.bddAbove_image (hf.comp <| Continuous.Prod.mk x').continuousOn
[GOAL]
case inr.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ (y_1 : β), y_1 ∈ K → f x y_1 ≤ f x y
this : (∀ (a' : α), a' < f x y → ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ (a' : α), a' > f x y → ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z
[PROOFSTEP]
have h : ({ x } : Set γ) ×ˢ K ⊆ ↿f ⁻¹' Iio z :=
  by
  rintro ⟨x', y'⟩ ⟨(rfl : x' = x), hy'⟩
  exact (hy y' hy').trans_lt hz
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ (y_1 : β), y_1 ∈ K → f x y_1 ≤ f x y
this : (∀ (a' : α), a' < f x y → ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ (a' : α), a' > f x y → ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
⊢ {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
[PROOFSTEP]
rintro ⟨x', y'⟩ ⟨(rfl : x' = x), hy'⟩
[GOAL]
case mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
y : β
hyK : y ∈ K
z : α
x' : γ
y' : β
hy' : (x', y').snd ∈ K
h2y : sSup ((fun y => f x' y) '' K) = f x' y
hy : ∀ (y_1 : β), y_1 ∈ K → f x' y_1 ≤ f x' y
this :
  (∀ (a' : α), a' < f x' y → ∀ᶠ (b : γ) in 𝓝 x', a' < f b y) ∧ ∀ (a' : α), a' > f x' y → ∀ᶠ (b : γ) in 𝓝 x', f b y < a'
hz : z > f x' y
⊢ (x', y') ∈ ↿f ⁻¹' Iio z
[PROOFSTEP]
exact (hy y' hy').trans_lt hz
[GOAL]
case inr.intro.intro.intro.refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ (y_1 : β), y_1 ∈ K → f x y_1 ≤ f x y
this : (∀ (a' : α), a' < f x y → ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ (a' : α), a' > f x y → ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z
[PROOFSTEP]
obtain ⟨u, v, hu, _, hxu, hKv, huv⟩ := generalized_tube_lemma isCompact_singleton hK (isOpen_Iio.preimage hf) h
[GOAL]
case inr.intro.intro.intro.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ (y_1 : β), y_1 ∈ K → f x y_1 ≤ f x y
this : (∀ (a' : α), a' < f x y → ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ (a' : α), a' > f x y → ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen u
left✝ : IsOpen v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
⊢ ∀ᶠ (b : γ) in 𝓝 x, sSup (f b '' K) < z
[PROOFSTEP]
refine' eventually_of_mem (hu.mem_nhds (singleton_subset_iff.mp hxu)) fun x' hx' => _
[GOAL]
case inr.intro.intro.intro.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ (y_1 : β), y_1 ∈ K → f x y_1 ≤ f x y
this : (∀ (a' : α), a' < f x y → ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ (a' : α), a' > f x y → ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen u
left✝ : IsOpen v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
x' : γ
hx' : x' ∈ u
⊢ sSup (f x' '' K) < z
[PROOFSTEP]
rw [hK.sSup_lt_iff_of_continuous h0K (show Continuous (f x') from hf.comp <| Continuous.Prod.mk x').continuousOn]
[GOAL]
case inr.intro.intro.intro.refine'_2.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁴ : ConditionallyCompleteLinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : γ → β → α
K : Set β
hK : IsCompact K
hf : Continuous ↿f
h0K : Set.Nonempty K
x : γ
y : β
hyK : y ∈ K
h2y : sSup ((fun y => f x y) '' K) = f x y
hy : ∀ (y_1 : β), y_1 ∈ K → f x y_1 ≤ f x y
this : (∀ (a' : α), a' < f x y → ∀ᶠ (b : γ) in 𝓝 x, a' < f b y) ∧ ∀ (a' : α), a' > f x y → ∀ᶠ (b : γ) in 𝓝 x, f b y < a'
z : α
hz : z > f x y
h : {x} ×ˢ K ⊆ ↿f ⁻¹' Iio z
u : Set γ
v : Set β
hu : IsOpen u
left✝ : IsOpen v
hxu : {x} ⊆ u
hKv : K ⊆ v
huv : u ×ˢ v ⊆ ↿f ⁻¹' Iio z
x' : γ
hx' : x' ∈ u
⊢ ∀ (x : β), x ∈ K → f x' x < z
[PROOFSTEP]
exact fun y' hy' => huv (mk_mem_prod hx' (hKv hy'))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f [[a, b]]
⊢ f '' [[a, b]] = [[sInf (f '' [[a, b]]), sSup (f '' [[a, b]])]]
[PROOFSTEP]
refine' h.image_uIcc_eq_Icc.trans (uIcc_of_le _).symm
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f [[a, b]]
⊢ sInf (f '' [[a, b]]) ≤ sSup (f '' [[a, b]])
[PROOFSTEP]
refine' csInf_le_csSup _ _ (nonempty_uIcc.image _)
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (f '' [[a, b]])
[PROOFSTEP]
rw [h.image_uIcc_eq_Icc]
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (f '' [[a, b]])
[PROOFSTEP]
rw [h.image_uIcc_eq_Icc]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f [[a, b]]
⊢ BddBelow (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
case refine'_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f [[a, b]]
⊢ BddAbove (Icc (sInf (f '' [[a, b]])) (sSup (f '' [[a, b]])))
[PROOFSTEP]
exacts [bddBelow_Icc, bddAbove_Icc]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
⊢ sInf (f '' Icc a b) ≤ f c
[PROOFSTEP]
have := mem_image_of_mem f hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ sInf (f '' Icc a b) ≤ f c
[PROOFSTEP]
rw [h.image_Icc (hc.1.trans hc.2)] at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ sInf (f '' Icc a b) ≤ f c
[PROOFSTEP]
exact this.1
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
⊢ f c ≤ sSup (f '' Icc a b)
[PROOFSTEP]
have := mem_image_of_mem f hc
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ f '' Icc a b
⊢ f c ≤ sSup (f '' Icc a b)
[PROOFSTEP]
rw [h.image_Icc (hc.1.trans hc.2)] at this
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : ConditionallyCompleteLinearOrder α
inst✝⁶ : TopologicalSpace α
inst✝⁵ : OrderTopology α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : DenselyOrdered α
inst✝¹ : ConditionallyCompleteLinearOrder β
inst✝ : OrderTopology β
f : α → β
a b c : α
h : ContinuousOn f (Icc a b)
hc : c ∈ Icc a b
this : f c ∈ Icc (sInf (f '' Icc a b)) (sSup (f '' Icc a b))
⊢ f c ≤ sSup (f '' Icc a b)
[PROOFSTEP]
exact this.2


[GOAL]
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ SupConvergenceClass α
[PROOFSTEP]
refine' ⟨fun a s ha => tendsto_order.2 ⟨fun b hb => _, fun b hb => _⟩⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
⊢ ∀ᶠ (b_1 : ↑s) in atTop, b < CoeTC.coe b_1
[PROOFSTEP]
rcases ha.exists_between hb with ⟨c, hcs, bc, bca⟩
[GOAL]
case refine'_1.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
c : α
hcs : c ∈ s
bc : b < c
bca : c ≤ a
⊢ ∀ᶠ (b_1 : ↑s) in atTop, b < CoeTC.coe b_1
[PROOFSTEP]
lift c to s using hcs
[GOAL]
case refine'_1.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b < a
c : { x // x ∈ s }
bc : b < ↑c
bca : ↑c ≤ a
⊢ ∀ᶠ (b_1 : ↑s) in atTop, b < CoeTC.coe b_1
[PROOFSTEP]
refine' (eventually_ge_atTop c).mono fun x hx => bc.trans_le hx
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
a : α
s : Set α
ha : IsLUB s a
b : α
hb : b > a
⊢ ∀ᶠ (b_1 : ↑s) in atTop, CoeTC.coe b_1 < b
[PROOFSTEP]
exact eventually_of_forall fun x => (ha.1 x.2).trans_lt hb
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto f atTop (𝓝 a)
[PROOFSTEP]
suffices : Tendsto (rangeFactorization f) atTop atTop
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
this : Tendsto (rangeFactorization f) atTop atTop
⊢ Tendsto f atTop (𝓝 a)
case this
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop
[PROOFSTEP]
exact (SupConvergenceClass.tendsto_coe_atTop_isLUB _ _ ha).comp this
[GOAL]
case this
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsLUB (range f) a
⊢ Tendsto (rangeFactorization f) atTop atTop
[PROOFSTEP]
exact h_mono.rangeFactorization.tendsto_atTop_atTop fun b => b.2.imp fun a ha => ha.ge
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsLUB (range f) a
⊢ Tendsto f atBot (𝓝 a)
[PROOFSTEP]
convert tendsto_atTop_isLUB h_anti.dual_left ha using 1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
ha : IsGLB (range f) a
⊢ Tendsto f atBot (𝓝 a)
[PROOFSTEP]
convert tendsto_atTop_isLUB h_mono.dual ha.dual using 1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
ha : IsGLB (range f) a
⊢ Tendsto f atTop (𝓝 a)
[PROOFSTEP]
convert tendsto_atBot_isLUB h_anti.dual ha.dual using 1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
hbdd : BddAbove (range f)
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
hbdd : BddAbove (range f)
h✝ : IsEmpty ι
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
case inr
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
hbdd : BddAbove (range f)
h✝ : Nonempty ι
⊢ Tendsto f atTop (𝓝 (⨆ (i : ι), f i))
[PROOFSTEP]
exacts [tendsto_of_isEmpty, tendsto_atTop_isLUB h_mono (isLUB_ciSup hbdd)]
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : SupConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
hbdd : BddAbove (range f)
⊢ Tendsto f atBot (𝓝 (⨆ (i : ι), f i))
[PROOFSTEP]
convert tendsto_atTop_ciSup h_anti.dual hbdd.dual using 1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_mono : Monotone f
hbdd : BddBelow (range f)
⊢ Tendsto f atBot (𝓝 (⨅ (i : ι), f i))
[PROOFSTEP]
convert tendsto_atTop_ciSup h_mono.dual hbdd.dual using 1
[GOAL]
α : Type u_1
β : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
inst✝² : TopologicalSpace α
inst✝¹ : ConditionallyCompleteLattice α
inst✝ : InfConvergenceClass α
f : ι → α
a : α
h_anti : Antitone f
hbdd : BddBelow (range f)
⊢ Tendsto f atTop (𝓝 (⨅ (i : ι), f i))
[PROOFSTEP]
convert tendsto_atBot_ciSup h_anti.dual hbdd.dual using 1
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
⊢ SupConvergenceClass (α × β)
[PROOFSTEP]
constructor
[GOAL]
case tendsto_coe_atTop_isLUB
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
⊢ ∀ (a : α × β) (s : Set (α × β)), IsLUB s a → Tendsto CoeTC.coe atTop (𝓝 a)
[PROOFSTEP]
rintro ⟨a, b⟩ s h
[GOAL]
case tendsto_coe_atTop_isLUB.mk
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB s (a, b)
⊢ Tendsto CoeTC.coe atTop (𝓝 (a, b))
[PROOFSTEP]
rw [isLUB_prod, ← range_restrict, ← range_restrict] at h
[GOAL]
case tendsto_coe_atTop_isLUB.mk
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (restrict s fst)) (a, b).fst ∧ IsLUB (range (restrict s snd)) (a, b).snd
⊢ Tendsto CoeTC.coe atTop (𝓝 (a, b))
[PROOFSTEP]
have A : Tendsto (fun x : s => (x : α × β).1) atTop (𝓝 a) := tendsto_atTop_isLUB (monotone_fst.restrict s) h.1
[GOAL]
case tendsto_coe_atTop_isLUB.mk
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (restrict s fst)) (a, b).fst ∧ IsLUB (range (restrict s snd)) (a, b).snd
A : Tendsto (fun x => (↑x).fst) atTop (𝓝 a)
⊢ Tendsto CoeTC.coe atTop (𝓝 (a, b))
[PROOFSTEP]
have B : Tendsto (fun x : s => (x : α × β).2) atTop (𝓝 b) := tendsto_atTop_isLUB (monotone_snd.restrict s) h.2
[GOAL]
case tendsto_coe_atTop_isLUB.mk
α : Type u_1
β : Type u_2
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : SupConvergenceClass α
inst✝ : SupConvergenceClass β
a : α
b : β
s : Set (α × β)
h : IsLUB (range (restrict s fst)) (a, b).fst ∧ IsLUB (range (restrict s snd)) (a, b).snd
A : Tendsto (fun x => (↑x).fst) atTop (𝓝 a)
B : Tendsto (fun x => (↑x).snd) atTop (𝓝 b)
⊢ Tendsto CoeTC.coe atTop (𝓝 (a, b))
[PROOFSTEP]
convert A.prod_mk_nhds B
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
⊢ SupConvergenceClass ((i : ι) → α i)
[PROOFSTEP]
refine' ⟨fun f s h => _⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
f : (i : ι) → α i
s : Set ((i : ι) → α i)
h : IsLUB s f
⊢ Tendsto CoeTC.coe atTop (𝓝 f)
[PROOFSTEP]
simp only [isLUB_pi, ← range_restrict] at h
[GOAL]
α✝ : Type u_1
β : Type u_2
ι : Type u_3
α : ι → Type u_4
inst✝² : (i : ι) → Preorder (α i)
inst✝¹ : (i : ι) → TopologicalSpace (α i)
inst✝ : ∀ (i : ι), SupConvergenceClass (α i)
f : (i : ι) → α i
s : Set ((i : ι) → α i)
h : ∀ (a : ι), IsLUB (range (restrict s (eval a))) (f a)
⊢ Tendsto CoeTC.coe atTop (𝓝 f)
[PROOFSTEP]
exact tendsto_pi_nhds.2 fun i => tendsto_atTop_isLUB ((monotone_eval _).restrict _) (h i)
[GOAL]
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) ↔ Tendsto (f ∘ φ) atTop (𝓝 l)
[PROOFSTEP]
constructor
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto f atTop (𝓝 l) → Tendsto (f ∘ φ) atTop (𝓝 l)
[PROOFSTEP]
intro h
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
⊢ Tendsto (f ∘ φ) atTop (𝓝 l) → Tendsto f atTop (𝓝 l)
[PROOFSTEP]
intro h
[GOAL]
case mp
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto f atTop (𝓝 l)
⊢ Tendsto (f ∘ φ) atTop (𝓝 l)
[PROOFSTEP]
exact h.comp hg
[GOAL]
case mpr
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
⊢ Tendsto f atTop (𝓝 l)
[PROOFSTEP]
rcases tendsto_of_monotone hf with (h' | ⟨l', hl'⟩)
[GOAL]
case mpr.inl
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
h' : Tendsto f atTop atTop
⊢ Tendsto f atTop (𝓝 l)
[PROOFSTEP]
exact (not_tendsto_atTop_of_tendsto_nhds h (h'.comp hg)).elim
[GOAL]
case mpr.inr.intro
α✝ : Type u_1
β : Type u_2
ι₁ : Type u_3
ι₂ : Type u_4
α : Type u_5
inst✝⁶ : SemilatticeSup ι₁
inst✝⁵ : Preorder ι₂
inst✝⁴ : Nonempty ι₁
inst✝³ : TopologicalSpace α
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
f : ι₂ → α
φ : ι₁ → ι₂
l : α
hf : Monotone f
hg : Tendsto φ atTop atTop
h : Tendsto (f ∘ φ) atTop (𝓝 l)
l' : α
hl' : Tendsto f atTop (𝓝 l')
⊢ Tendsto f atTop (𝓝 l)
[PROOFSTEP]
rwa [tendsto_nhds_unique h (hl'.comp hg)]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ IsLUB (range f) a
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ upperBounds (range f)
[PROOFSTEP]
rintro _ ⟨b, rfl⟩
[GOAL]
case left.intro
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
b : β
⊢ f b ≤ a
[PROOFSTEP]
exact hf.ge_of_tendsto ha b
[GOAL]
case right
α : Type u_1
β : Type u_2
inst✝⁴ : TopologicalSpace α
inst✝³ : Preorder α
inst✝² : OrderClosedTopology α
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → α
a : α
hf : Monotone f
ha : Tendsto f atTop (𝓝 a)
⊢ a ∈ lowerBounds (upperBounds (range f))
[PROOFSTEP]
exact fun _ hb => le_of_tendsto' ha fun x => hb (Set.mem_range_self x)


[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
⊢ Continuous fun p => p.fst + p.snd
[PROOFSTEP]
refine' continuous_iff_continuousAt.2 _
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
⊢ ∀ (x : G × G), ContinuousAt (fun p => p.fst + p.snd) x
[PROOFSTEP]
rintro ⟨a, b⟩
[GOAL]
case mk
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b : G
⊢ ContinuousAt (fun p => p.fst + p.snd) (a, b)
[PROOFSTEP]
refine' LinearOrderedAddCommGroup.tendsto_nhds.2 fun ε ε0 => _
[GOAL]
case mk
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.fst + b_1.snd - (fun p => p.fst + p.snd) (a, b)| < ε
[PROOFSTEP]
rcases dense_or_discrete 0 ε with (⟨δ, δ0, δε⟩ | ⟨_h₁, h₂⟩)
[GOAL]
case mk.inl.intro.intro
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
δ : G
δ0 : 0 < δ
δε : δ < ε
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.fst + b_1.snd - (fun p => p.fst + p.snd) (a, b)| < ε
[PROOFSTEP]
filter_upwards [(eventually_abs_sub_lt a δ0).prod_nhds (eventually_abs_sub_lt b (sub_pos.2 δε))]
[GOAL]
case h
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
δ : G
δ0 : 0 < δ
δε : δ < ε
⊢ ∀ (a_1 : G × G), |a_1.fst - a| < δ ∧ |a_1.snd - b| < ε - δ → |a_1.fst + a_1.snd - (a + b)| < ε
[PROOFSTEP]
rintro ⟨x, y⟩ ⟨hx : |x - a| < δ, hy : |y - b| < ε - δ⟩
[GOAL]
case h.mk.intro
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
δ : G
δ0 : 0 < δ
δε : δ < ε
x y : G
hx : |x - a| < δ
hy : |y - b| < ε - δ
⊢ |(x, y).fst + (x, y).snd - (a + b)| < ε
[PROOFSTEP]
rw [add_sub_add_comm]
[GOAL]
case h.mk.intro
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
δ : G
δ0 : 0 < δ
δε : δ < ε
x y : G
hx : |x - a| < δ
hy : |y - b| < ε - δ
⊢ |(x, y).fst - a + ((x, y).snd - b)| < ε
[PROOFSTEP]
calc
  |x - a + (y - b)| ≤ |x - a| + |y - b| := abs_add _ _
  _ < δ + (ε - δ) := (add_lt_add hx hy)
  _ = ε := add_sub_cancel'_right _ _
[GOAL]
case mk.inr.intro
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
_h₁ : ∀ (a : G), 0 < a → ε ≤ a
h₂ : ∀ (a : G), a < ε → a ≤ 0
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.fst + b_1.snd - (fun p => p.fst + p.snd) (a, b)| < ε
[PROOFSTEP]
have hε : ∀ {x y}, |x - y| < ε → x = y := by
  intro x y h
  simpa [sub_eq_zero] using h₂ _ h
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
_h₁ : ∀ (a : G), 0 < a → ε ≤ a
h₂ : ∀ (a : G), a < ε → a ≤ 0
⊢ ∀ {x y : G}, |x - y| < ε → x = y
[PROOFSTEP]
intro x y h
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
_h₁ : ∀ (a : G), 0 < a → ε ≤ a
h₂ : ∀ (a : G), a < ε → a ≤ 0
x y : G
h : |x - y| < ε
⊢ x = y
[PROOFSTEP]
simpa [sub_eq_zero] using h₂ _ h
[GOAL]
case mk.inr.intro
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
_h₁ : ∀ (a : G), 0 < a → ε ≤ a
h₂ : ∀ (a : G), a < ε → a ≤ 0
hε : ∀ {x y : G}, |x - y| < ε → x = y
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.fst + b_1.snd - (fun p => p.fst + p.snd) (a, b)| < ε
[PROOFSTEP]
filter_upwards [(eventually_abs_sub_lt a ε0).prod_nhds (eventually_abs_sub_lt b ε0)]
[GOAL]
case h
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
_h₁ : ∀ (a : G), 0 < a → ε ≤ a
h₂ : ∀ (a : G), a < ε → a ≤ 0
hε : ∀ {x y : G}, |x - y| < ε → x = y
⊢ ∀ (a_1 : G × G), |a_1.fst - a| < ε ∧ |a_1.snd - b| < ε → |a_1.fst + a_1.snd - (a + b)| < ε
[PROOFSTEP]
rintro ⟨x, y⟩ ⟨hx : |x - a| < ε, hy : |y - b| < ε⟩
[GOAL]
case h.mk.intro
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a b ε : G
ε0 : ε > 0
_h₁ : ∀ (a : G), 0 < a → ε ≤ a
h₂ : ∀ (a : G), a < ε → a ≤ 0
hε : ∀ {x y : G}, |x - y| < ε → x = y
x y : G
hx : |x - a| < ε
hy : |y - b| < ε
⊢ |(x, y).fst + (x, y).snd - (a + b)| < ε
[PROOFSTEP]
simpa [hε hx, hε hy]
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f g : α → G
a ε : G
ε0 : ε > 0
x : G
hx : |x - a| < ε
⊢ |-x - (fun a => -a) a| < ε
[PROOFSTEP]
rwa [neg_sub_neg, abs_sub_comm]
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f✝ g f : α → G
⊢ Tendsto f l (𝓝 0) ↔ Tendsto (abs ∘ f) l (𝓝 0)
[PROOFSTEP]
refine' ⟨fun h => (abs_zero : |(0 : G)| = 0) ▸ h.abs, fun h => _⟩
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f✝ g f : α → G
h : Tendsto (abs ∘ f) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)
[PROOFSTEP]
have : Tendsto (fun a => -|f a|) l (𝓝 0) := (neg_zero : -(0 : G) = 0) ▸ h.neg
[GOAL]
α : Type u_1
G : Type u_2
inst✝² : TopologicalSpace G
inst✝¹ : LinearOrderedAddCommGroup G
inst✝ : OrderTopology G
l : Filter α
f✝ g f : α → G
h : Tendsto (abs ∘ f) l (𝓝 0)
this : Tendsto (fun a => -|f a|) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)
[PROOFSTEP]
exact tendsto_of_tendsto_of_tendsto_of_le_of_le this h (fun x => neg_abs_le_self <| f x) fun x => le_abs_self <| f x


[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂✝ a₂ : α
h : HasSum f a₁
⊢ HasSum (fun i => a₂ * f i) (a₂ * a₁)
[PROOFSTEP]
simpa only using h.map (AddMonoidHom.mulLeft a₂) (continuous_const.mul continuous_id)
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂✝ a₂ : α
hf : HasSum f a₁
⊢ HasSum (fun i => f i * a₂) (a₁ * a₂)
[PROOFSTEP]
simpa only using hf.map (AddMonoidHom.mulRight a₂) (continuous_id.mul continuous_const)
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : HasSum f a
b : α
⊢ HasSum (fun i => f i / b) (a / b)
[PROOFSTEP]
simp only [div_eq_mul_inv, h.mul_right b⁻¹]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a₂ ≠ 0
H : HasSum (fun i => a₂ * f i) (a₂ * a₁)
⊢ HasSum f a₁
[PROOFSTEP]
simpa only [inv_mul_cancel_left₀ h] using H.mul_left a₂⁻¹
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a₂ ≠ 0
H : HasSum (fun i => f i * a₂) (a₁ * a₂)
⊢ HasSum f a₁
[PROOFSTEP]
simpa only [mul_inv_cancel_right₀ h] using H.mul_right a₂⁻¹
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a₂ ≠ 0
⊢ HasSum (fun i => f i / a₂) (a₁ / a₂) ↔ HasSum f a₁
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hasSum_mul_right_iff (inv_ne_zero h)
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a ≠ 0
H : Summable fun i => a * f i
⊢ Summable f
[PROOFSTEP]
simpa only [inv_mul_cancel_left₀ h] using H.mul_left a⁻¹
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a ≠ 0
H : Summable fun i => f i * a
⊢ Summable f
[PROOFSTEP]
simpa only [mul_inv_cancel_right₀ h] using H.mul_right a⁻¹
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝² : DivisionSemiring α
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
h : a ≠ 0
⊢ (Summable fun i => f i / a) ↔ Summable f
[PROOFSTEP]
simpa only [div_eq_mul_inv] using summable_mul_right_iff (inv_ne_zero h)
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
ha : a = 0
⊢ ∑' (x : ι), a * f x = a * ∑' (x : ι), f x
[PROOFSTEP]
simp [ha]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
ha : ¬a = 0
⊢ ∑' (x : ι), a * f x = a * ∑' (x : ι), f x
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt (summable_mul_left_iff ha).mp hf), mul_zero]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
ha : a = 0
⊢ ∑' (x : ι), f x * a = (∑' (x : ι), f x) * a
[PROOFSTEP]
simp [ha]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
hf : ¬Summable f
ha : ¬a = 0
⊢ ∑' (x : ι), f x * a = (∑' (x : ι), f x) * a
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable (mt (summable_mul_right_iff ha).mp hf), zero_mul]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : DivisionSemiring α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalSemiring α
f g : ι → α
a a₁ a₂ : α
inst✝ : T2Space α
⊢ ∑' (x : ι), f x / a = (∑' (x : ι), f x) / a
[PROOFSTEP]
simpa only [div_eq_mul_inv] using tsum_mul_right
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f x.fst * g x.snd
⊢ Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
rw [summable_mul_prod_iff_summable_mul_sigma_antidiagonal] at h
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
⊢ Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
conv => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
| Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
| Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
| Summable fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
congr
[GOAL]
case f
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
| fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
ext
[GOAL]
case f.h
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
x✝ : ℕ
| ∑ kl in Nat.antidiagonal x✝, f kl.fst * g kl.snd
[PROOFSTEP]
rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f (↑x.snd).fst * g (↑x.snd).snd
⊢ Summable fun x => ∑' (b : ↑↑(Nat.antidiagonal x)), f (↑b).fst * g (↑b).snd
[PROOFSTEP]
exact h.sigma' fun n => (hasSum_fintype _).summable
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
conv_rhs => congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
| ∑' (n : ℕ), ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
| ∑' (n : ℕ), ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
congr; ext; rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
| ∑' (n : ℕ), ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
congr
[GOAL]
case f
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
| fun n => ∑ kl in Nat.antidiagonal n, f kl.fst * g kl.snd
[PROOFSTEP]
ext
[GOAL]
case f.h
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
x✝ : ℕ
| ∑ kl in Nat.antidiagonal x✝, f kl.fst * g kl.snd
[PROOFSTEP]
rw [← Finset.sum_finset_coe, ← tsum_fintype]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (x : ℕ) (b : ↑↑(Nat.antidiagonal x)), f (↑b).fst * g (↑b).snd
[PROOFSTEP]
rw [tsum_mul_tsum hf hg hfg, ← Nat.sigmaAntidiagonalEquivProd.tsum_eq (_ : ℕ × ℕ → α)]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ ∑' (c : (n : ℕ) × { x // x ∈ Nat.antidiagonal n }),
      f (↑Nat.sigmaAntidiagonalEquivProd c).fst * g (↑Nat.sigmaAntidiagonalEquivProd c).snd =
    ∑' (x : ℕ) (b : ↑↑(Nat.antidiagonal x)), f (↑b).fst * g (↑b).snd
[PROOFSTEP]
exact tsum_sigma' (fun n => (hasSum_fintype _).summable) (summable_mul_prod_iff_summable_mul_sigma_antidiagonal.mp hfg)
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f x.fst * g x.snd
⊢ Summable fun n => ∑ k in range (n + 1), f k * g (n - k)
[PROOFSTEP]
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
h : Summable fun x => f x.fst * g x.snd
⊢ Summable fun n => ∑ ij in Nat.antidiagonal n, f ij.fst * g ij.snd
[PROOFSTEP]
exact summable_sum_mul_antidiagonal_of_summable_mul h
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ k in range (n + 1), f k * g (n - k)
[PROOFSTEP]
simp_rw [← Nat.sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]
[GOAL]
ι : Type u_1
κ : Type u_2
R : Type u_3
α : Type u_4
inst✝³ : TopologicalSpace α
inst✝² : NonUnitalNonAssocSemiring α
f g : ℕ → α
inst✝¹ : T3Space α
inst✝ : TopologicalSemiring α
hf : Summable f
hg : Summable g
hfg : Summable fun x => f x.fst * g x.snd
⊢ (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ ij in Nat.antidiagonal n, f ij.fst * g ij.snd
[PROOFSTEP]
exact tsum_mul_tsum_eq_tsum_sum_antidiagonal hf hg hfg