[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
⊢ β
[PROOFSTEP]
classical
haveI : Nonempty β := ⟨f a⟩
letI : TopologicalSpace α := Preorder.topology α
exact if 𝓝[<] a = ⊥ ∨ ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y) then f a else limUnder (𝓝[<] a) f
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
⊢ β
[PROOFSTEP]
haveI : Nonempty β := ⟨f a⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
this : Nonempty β
⊢ β
[PROOFSTEP]
letI : TopologicalSpace α := Preorder.topology α
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
f : α → β
a : α
this✝ : Nonempty β
this : TopologicalSpace α := Preorder.topology α
⊢ β
[PROOFSTEP]
exact if 𝓝[<] a = ⊥ ∨ ¬∃ y, Tendsto f (𝓝[<] a) (𝓝 y) then f a else limUnder (𝓝[<] a) f
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ leftLim f a = y
[PROOFSTEP]
have h'' : ∃ y, Tendsto f (𝓝[<] a) (𝓝 y) := ⟨y, h'⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ leftLim f a = y
[PROOFSTEP]
rw [h'α.topology_eq_generate_intervals] at h h' h''
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ leftLim f a = y
[PROOFSTEP]
simp only [leftLim, h, h'', not_true, or_self_iff, if_false]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
⊢ limUnder (𝓝[Iio a] a) f = y
[PROOFSTEP]
haveI := neBot_iff.2 h
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : LinearOrder α
inst✝¹ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
inst✝ : T2Space β
f : α → β
a : α
y : β
h : 𝓝[Iio a] a ≠ ⊥
h' : Tendsto f (𝓝[Iio a] a) (𝓝 y)
h'' : ∃ y, Tendsto f (𝓝[Iio a] a) (𝓝 y)
this : NeBot (𝓝[Iio a] a)
⊢ limUnder (𝓝[Iio a] a) f = y
[PROOFSTEP]
exact lim_eq h'
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[Iio a] a = ⊥
⊢ leftLim f a = f a
[PROOFSTEP]
rw [h'α.topology_eq_generate_intervals] at h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : TopologicalSpace β
hα : TopologicalSpace α
h'α : OrderTopology α
f : α → β
a : α
h : 𝓝[Iio a] a = ⊥
⊢ leftLim f a = f a
[PROOFSTEP]
simp [leftLim, ite_eq_left_iff, h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ leftLim f x ≤ f y
[PROOFSTEP]
letI : TopologicalSpace α := Preorder.topology α
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this : TopologicalSpace α := Preorder.topology α
⊢ leftLim f x ≤ f y
[PROOFSTEP]
haveI : OrderTopology α := ⟨rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ leftLim f x ≤ f y
[PROOFSTEP]
rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio x] x = ⊥
⊢ leftLim f x ≤ f y
[PROOFSTEP]
simpa [leftLim, h'] using hf h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio x] x ≠ ⊥
⊢ leftLim f x ≤ f y
[PROOFSTEP]
haveI A : NeBot (𝓝[<] x) := neBot_iff.2 h'
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
⊢ leftLim f x ≤ f y
[PROOFSTEP]
rw [leftLim_eq_sSup hf h']
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
⊢ sSup (f '' Iio x) ≤ f y
[PROOFSTEP]
refine' csSup_le _ _
[GOAL]
case inr.refine'_1
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
⊢ Set.Nonempty (f '' Iio x)
[PROOFSTEP]
simp only [nonempty_image_iff]
[GOAL]
case inr.refine'_1
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
⊢ Set.Nonempty (Iio x)
[PROOFSTEP]
exact (forall_mem_nonempty_iff_neBot.2 A) _ self_mem_nhdsWithin
[GOAL]
case inr.refine'_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
⊢ ∀ (b : β), b ∈ f '' Iio x → b ≤ f y
[PROOFSTEP]
simp only [mem_image, mem_Iio, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂]
[GOAL]
case inr.refine'_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
⊢ ∀ (a : α), a < x → f a ≤ f y
[PROOFSTEP]
intro z hz
[GOAL]
case inr.refine'_2
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio x] x ≠ ⊥
A : NeBot (𝓝[Iio x] x)
z : α
hz : z < x
⊢ f z ≤ f y
[PROOFSTEP]
exact hf (hz.le.trans h)
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
⊢ f x ≤ leftLim f y
[PROOFSTEP]
letI : TopologicalSpace α := Preorder.topology α
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this : TopologicalSpace α := Preorder.topology α
⊢ f x ≤ leftLim f y
[PROOFSTEP]
haveI : OrderTopology α := ⟨rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ f x ≤ leftLim f y
[PROOFSTEP]
rcases eq_or_ne (𝓝[<] y) ⊥ with (h' | h')
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y = ⊥
⊢ f x ≤ leftLim f y
[PROOFSTEP]
rw [leftLim_eq_of_eq_bot _ h']
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y = ⊥
⊢ f x ≤ f y
[PROOFSTEP]
exact hf h.le
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y ≠ ⊥
⊢ f x ≤ leftLim f y
[PROOFSTEP]
rw [leftLim_eq_sSup hf h']
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y ≠ ⊥
⊢ f x ≤ sSup (f '' Iio y)
[PROOFSTEP]
refine' le_csSup ⟨f y, _⟩ (mem_image_of_mem _ h)
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y ≠ ⊥
⊢ f y ∈ upperBounds (f '' Iio y)
[PROOFSTEP]
simp only [upperBounds, mem_image, mem_Iio, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, mem_setOf_eq]
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y ≠ ⊥
⊢ ∀ (a : α), a < y → f a ≤ f y
[PROOFSTEP]
intro z hz
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y ≠ ⊥
z : α
hz : z < y
⊢ f z ≤ f y
[PROOFSTEP]
exact hf hz.le
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
⊢ Monotone (leftLim f)
[PROOFSTEP]
intro x y h
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y✝ x y : α
h : x ≤ y
⊢ leftLim f x ≤ leftLim f y
[PROOFSTEP]
rcases eq_or_lt_of_le h with (rfl | hxy)
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y x : α
h : x ≤ x
⊢ leftLim f x ≤ leftLim f x
[PROOFSTEP]
exact le_rfl
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y✝ x y : α
h : x ≤ y
hxy : x < y
⊢ leftLim f x ≤ leftLim f y
[PROOFSTEP]
exact (hf.leftLim_le le_rfl).trans (hf.le_leftLim hxy)
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
⊢ rightLim f x ≤ leftLim f y
[PROOFSTEP]
letI : TopologicalSpace α := Preorder.topology α
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this : TopologicalSpace α := Preorder.topology α
⊢ rightLim f x ≤ leftLim f y
[PROOFSTEP]
haveI : OrderTopology α := ⟨rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
⊢ rightLim f x ≤ leftLim f y
[PROOFSTEP]
rcases eq_or_ne (𝓝[<] y) ⊥ with (h' | h')
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y = ⊥
⊢ rightLim f x ≤ leftLim f y
[PROOFSTEP]
simp [leftLim, h']
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y = ⊥
⊢ rightLim f x ≤ f y
[PROOFSTEP]
exact rightLim_le hf h
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y ≠ ⊥
⊢ rightLim f x ≤ leftLim f y
[PROOFSTEP]
obtain ⟨a, ⟨xa, ay⟩⟩ : (Ioo x y).Nonempty :=
  forall_mem_nonempty_iff_neBot.2 (neBot_iff.2 h') (Ioo x y) (Ioo_mem_nhdsWithin_Iio ⟨h, le_refl _⟩)
[GOAL]
case inr.intro.intro
α : Type u_1
β : Type u_2
inst✝³ : LinearOrder α
inst✝² : ConditionallyCompleteLinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
h : x < y
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
h' : 𝓝[Iio y] y ≠ ⊥
a : α
xa : x < a
ay : a < y
⊢ rightLim f x ≤ leftLim f y
[PROOFSTEP]
calc
  rightLim f x ≤ f a := hf.rightLim_le xa
  _ ≤ leftLim f y := hf.le_leftLim ay
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
[PROOFSTEP]
rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[Iio x] x = ⊥
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
[PROOFSTEP]
simp [h']
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[Iio x] x ≠ ⊥
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
[PROOFSTEP]
rw [leftLim_eq_sSup hf h']
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
h' : 𝓝[Iio x] x ≠ ⊥
⊢ Tendsto f (𝓝[Iio x] x) (𝓝 (sSup (f '' Iio x)))
[PROOFSTEP]
exact hf.tendsto_nhdsWithin_Iio x
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
⊢ Tendsto f (𝓝[Iio x] x) (𝓝[Iic (leftLim f x)] leftLim f x)
[PROOFSTEP]
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within f (hf.tendsto_leftLim x)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
x : α
⊢ ∀ᶠ (x_1 : α) in 𝓝[Iio x] x, f x_1 ∈ Iic (leftLim f x)
[PROOFSTEP]
filter_upwards [@self_mem_nhdsWithin _ _ x (Iio x)] with y hy using hf.le_leftLim hy
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
[PROOFSTEP]
rcases eq_or_ne (𝓝[<] x) ⊥ with (h' | h')
[GOAL]
case inl
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[Iio x] x = ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
[PROOFSTEP]
simp [leftLim_eq_of_eq_bot f h', ContinuousWithinAt, h']
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[Iio x] x ≠ ⊥
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
[PROOFSTEP]
haveI : (𝓝[Iio x] x).NeBot := neBot_iff.2 h'
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[Iio x] x ≠ ⊥
this : NeBot (𝓝[Iio x] x)
⊢ ContinuousWithinAt f (Iio x) x ↔ leftLim f x = f x
[PROOFSTEP]
refine' ⟨fun h => tendsto_nhds_unique (hf.tendsto_leftLim x) h.tendsto, fun h => _⟩
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[Iio x] x ≠ ⊥
this : NeBot (𝓝[Iio x] x)
h : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x
[PROOFSTEP]
have := hf.tendsto_leftLim x
[GOAL]
case inr
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h' : 𝓝[Iio x] x ≠ ⊥
this✝ : NeBot (𝓝[Iio x] x)
h : leftLim f x = f x
this : Tendsto f (𝓝[Iio x] x) (𝓝 (leftLim f x))
⊢ ContinuousWithinAt f (Iio x) x
[PROOFSTEP]
rwa [h] at this
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
⊢ ContinuousAt f x ↔ leftLim f x = rightLim f x
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : ContinuousAt f x
⊢ leftLim f x = rightLim f x
[PROOFSTEP]
have A : leftLim f x = f x := hf.continuousWithinAt_Iio_iff_leftLim_eq.1 h.continuousWithinAt
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : ContinuousAt f x
A : leftLim f x = f x
⊢ leftLim f x = rightLim f x
[PROOFSTEP]
have B : rightLim f x = f x := hf.continuousWithinAt_Ioi_iff_rightLim_eq.1 h.continuousWithinAt
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : ContinuousAt f x
A : leftLim f x = f x
B : rightLim f x = f x
⊢ leftLim f x = rightLim f x
[PROOFSTEP]
exact A.trans B.symm
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ ContinuousAt f x
[PROOFSTEP]
have h' : leftLim f x = f x := by
  apply le_antisymm (leftLim_le hf (le_refl _))
  rw [h]
  exact le_rightLim hf (le_refl _)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ leftLim f x = f x
[PROOFSTEP]
apply le_antisymm (leftLim_le hf (le_refl _))
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ f x ≤ leftLim f x
[PROOFSTEP]
rw [h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
⊢ f x ≤ rightLim f x
[PROOFSTEP]
exact le_rightLim hf (le_refl _)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousAt f x
[PROOFSTEP]
refine' continuousAt_iff_continuous_left'_right'.2 ⟨_, _⟩
[GOAL]
case refine'_2.refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousWithinAt f (Iio x) x
[PROOFSTEP]
exact hf.continuousWithinAt_Iio_iff_leftLim_eq.2 h'
[GOAL]
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : leftLim f x = f x
⊢ ContinuousWithinAt f (Ioi x) x
[PROOFSTEP]
rw [h] at h'
[GOAL]
case refine'_2.refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : ConditionallyCompleteLinearOrder β
inst✝³ : TopologicalSpace β
inst✝² : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝¹ : TopologicalSpace α
inst✝ : OrderTopology α
h : leftLim f x = rightLim f x
h' : rightLim f x = f x
⊢ ContinuousWithinAt f (Ioi x) x
[PROOFSTEP]
exact hf.continuousWithinAt_Ioi_iff_rightLim_eq.2 h'
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
nontriviality α
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
let s := {x | ¬ContinuousWithinAt f (Ioi x) x}
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
have : ∀ x, x ∈ s → ∃ z, f x < z ∧ ∀ y, x < y → z ≤ f y :=
  by
  rintro x (hx : ¬ContinuousWithinAt f (Ioi x) x)
  contrapose! hx
  refine' tendsto_order.2 ⟨fun m hm => _, fun u hu => _⟩
  · filter_upwards [@self_mem_nhdsWithin _ _ x (Ioi x)] with y hy using hm.trans_le (hf (le_of_lt hy))
  rcases hx u hu with ⟨v, xv, fvu⟩
  have : Ioo x v ∈ 𝓝[>] x := Ioo_mem_nhdsWithin_Ioi ⟨le_refl _, xv⟩
  filter_upwards [this] with y hy
  apply (hf hy.2.le).trans_lt fvu
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
⊢ ∀ (x : α), x ∈ s → ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y
[PROOFSTEP]
rintro x (hx : ¬ContinuousWithinAt f (Ioi x) x)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
x : α
hx : ¬ContinuousWithinAt f (Ioi x) x
⊢ ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y
[PROOFSTEP]
contrapose! hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
⊢ ContinuousWithinAt f (Ioi x) x
[PROOFSTEP]
refine' tendsto_order.2 ⟨fun m hm => _, fun u hu => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
m : β
hm : m < f x
⊢ ∀ᶠ (b : α) in 𝓝[Ioi x] x, m < f b
[PROOFSTEP]
filter_upwards [@self_mem_nhdsWithin _ _ x (Ioi x)] with y hy using hm.trans_le (hf (le_of_lt hy))
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
⊢ ∀ᶠ (b : α) in 𝓝[Ioi x] x, f b < u
[PROOFSTEP]
rcases hx u hu with ⟨v, xv, fvu⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
v : α
xv : x < v
fvu : f v < u
⊢ ∀ᶠ (b : α) in 𝓝[Ioi x] x, f b < u
[PROOFSTEP]
have : Ioo x v ∈ 𝓝[>] x := Ioo_mem_nhdsWithin_Ioi ⟨le_refl _, xv⟩
[GOAL]
case refine'_2.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
v : α
xv : x < v
fvu : f v < u
this : Ioo x v ∈ 𝓝[Ioi x] x
⊢ ∀ᶠ (b : α) in 𝓝[Ioi x] x, f b < u
[PROOFSTEP]
filter_upwards [this] with y hy
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y✝ : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
x : α
hx : ∀ (z : β), f x < z → ∃ y, x < y ∧ f y < z
u : β
hu : u > f x
v : α
xv : x < v
fvu : f v < u
this : Ioo x v ∈ 𝓝[Ioi x] x
y : α
hy : y ∈ Ioo x v
⊢ f y < u
[PROOFSTEP]
apply (hf hy.2.le).trans_lt fvu
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
this : ∀ (x : α), x ∈ s → ∃ z, f x < z ∧ ∀ (y : α), x < y → z ≤ f y
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
choose! z hz using this
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
have I : InjOn f s := by
  apply StrictMonoOn.injOn
  intro x hx y _ hxy
  calc
    f x < z x := (hz x hx).1
    _ ≤ f y := (hz x hx).2 y hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
⊢ InjOn f s
[PROOFSTEP]
apply StrictMonoOn.injOn
[GOAL]
case H
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
⊢ StrictMonoOn f s
[PROOFSTEP]
intro x hx y _ hxy
[GOAL]
case H
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝¹ y✝ : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
x : α
hx : x ∈ s
y : α
x✝ : y ∈ s
hxy : x < y
⊢ f x < f y
[PROOFSTEP]
calc
  f x < z x := (hz x hx).1
  _ ≤ f y := (hz x hx).2 y hxy
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
have fs_count : (f '' s).Countable :=
  by
  have A : (f '' s).PairwiseDisjoint fun x => Ioo x (z (invFunOn f s x)) :=
    by
    rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv
    wlog hle : u ≤ v generalizing u v
    · exact (this v vs u us huv.symm (le_of_not_le hle)).symm
    have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
    apply disjoint_iff_forall_ne.2
    rintro a ha b hb rfl
    simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb
    exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v hlt)).trans hb.1)
  apply Set.PairwiseDisjoint.countable_of_Ioo A
  rintro _ ⟨y, ys, rfl⟩
  simpa only [I.leftInvOn_invFunOn ys] using (hz y ys).1
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
⊢ Set.Countable (f '' s)
[PROOFSTEP]
have A : (f '' s).PairwiseDisjoint fun x => Ioo x (z (invFunOn f s x)) :=
  by
  rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv
  wlog hle : u ≤ v generalizing u v
  · exact (this v vs u us huv.symm (le_of_not_le hle)).symm
  have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
  apply disjoint_iff_forall_ne.2
  rintro a ha b hb rfl
  simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb
  exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v hlt)).trans hb.1)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
⊢ PairwiseDisjoint (f '' s) fun x => Ioo x (z (invFunOn f s x))
[PROOFSTEP]
rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
⊢ (Disjoint on fun x => Ioo x (z (invFunOn f s x))) (f u) (f v)
[PROOFSTEP]
wlog hle : u ≤ v generalizing u v
[GOAL]
case intro.intro.intro.intro.inr
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
this :
  ∀ (u : α),
    u ∈ s → ∀ (v : α), v ∈ s → f u ≠ f v → u ≤ v → (Disjoint on fun x => Ioo x (z (invFunOn f s x))) (f u) (f v)
hle : ¬u ≤ v
⊢ (Disjoint on fun x => Ioo x (z (invFunOn f s x))) (f u) (f v)
[PROOFSTEP]
exact (this v vs u us huv.symm (le_of_not_le hle)).symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
⊢ (Disjoint on fun x => Ioo x (z (invFunOn f s x))) (f u) (f v)
[PROOFSTEP]
have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
⊢ (Disjoint on fun x => Ioo x (z (invFunOn f s x))) (f u) (f v)
[PROOFSTEP]
apply disjoint_iff_forall_ne.2
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
⊢ ∀ ⦃a : β⦄,
    a ∈ (fun x => Ioo x (z (invFunOn f s x))) (f u) → ∀ ⦃b : β⦄, b ∈ (fun x => Ioo x (z (invFunOn f s x))) (f v) → a ≠ b
[PROOFSTEP]
rintro a ha b hb rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
a : β
ha : a ∈ (fun x => Ioo x (z (invFunOn f s x))) (f u)
hb : a ∈ (fun x => Ioo x (z (invFunOn f s x))) (f v)
⊢ False
[PROOFSTEP]
simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
u : α
us : u ∈ s
v : α
vs : v ∈ s
huv : f u ≠ f v
hle : u ≤ v
hlt : u < v
a : β
ha : a ∈ Ioo (f u) (z u)
hb : a ∈ Ioo (f v) (z v)
⊢ False
[PROOFSTEP]
exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v hlt)).trans hb.1)
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
A : PairwiseDisjoint (f '' s) fun x => Ioo x (z (invFunOn f s x))
⊢ Set.Countable (f '' s)
[PROOFSTEP]
apply Set.PairwiseDisjoint.countable_of_Ioo A
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
A : PairwiseDisjoint (f '' s) fun x => Ioo x (z (invFunOn f s x))
⊢ ∀ (x : β), x ∈ f '' s → x < z (invFunOn f s x)
[PROOFSTEP]
rintro _ ⟨y, ys, rfl⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y✝ : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
A : PairwiseDisjoint (f '' s) fun x => Ioo x (z (invFunOn f s x))
y : α
ys : y ∈ s
⊢ f y < z (invFunOn f s (f y))
[PROOFSTEP]
simpa only [I.leftInvOn_invFunOn ys] using (hz y ys).1
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
✝ : Nontrivial α
s : Set α := {x | ¬ContinuousWithinAt f (Ioi x) x}
z : α → β
hz : ∀ (x : α), x ∈ s → f x < z x ∧ ∀ (y : α), x < y → z x ≤ f y
I : InjOn f s
fs_count : Set.Countable (f '' s)
⊢ Set.Countable {x | ¬ContinuousWithinAt f (Ioi x) x}
[PROOFSTEP]
exact MapsTo.countable_of_injOn (mapsTo_image f s) I fs_count
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
⊢ Set.Countable {x | ¬ContinuousAt f x}
[PROOFSTEP]
apply (hf.countable_not_continuousWithinAt_Ioi.union hf.countable_not_continuousWithinAt_Iio).mono _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
⊢ {x | ¬ContinuousAt f x} ⊆ {x | ¬ContinuousWithinAt f (Ioi x) x} ∪ {x | ¬ContinuousWithinAt f (Iio x) x}
[PROOFSTEP]
refine' compl_subset_compl.1 _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
⊢ ({x | ¬ContinuousWithinAt f (Ioi x) x} ∪ {x | ¬ContinuousWithinAt f (Iio x) x})ᶜ ⊆ {x | ¬ContinuousAt f x}ᶜ
[PROOFSTEP]
simp only [compl_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
⊢ {x | ¬ContinuousWithinAt f (Ioi x) x}ᶜ ∩ {x | ¬ContinuousWithinAt f (Iio x) x}ᶜ ⊆ {x | ¬ContinuousAt f x}ᶜ
[PROOFSTEP]
rintro x ⟨hx, h'x⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
x : α
hx : x ∈ {x | ¬ContinuousWithinAt f (Ioi x) x}ᶜ
h'x : x ∈ {x | ¬ContinuousWithinAt f (Iio x) x}ᶜ
⊢ x ∈ {x | ¬ContinuousAt f x}ᶜ
[PROOFSTEP]
simp only [mem_setOf_eq, Classical.not_not, mem_compl_iff] at hx h'x ⊢
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : ConditionallyCompleteLinearOrder β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
f : α → β
hf : Monotone f
x✝ y : α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : TopologicalSpace.SecondCountableTopology β
x : α
hx : ContinuousWithinAt f (Ioi x) x
h'x : ContinuousWithinAt f (Iio x) x
⊢ ContinuousAt f x
[PROOFSTEP]
exact continuousAt_iff_continuous_left'_right'.2 ⟨h'x, hx⟩


[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum f a₁
hg : HasSum g a₂
⊢ a₁ ≤ a₂
[PROOFSTEP]
rw [← hasSum_extend_zero he] at hf
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
⊢ a₁ ≤ a₂
[PROOFSTEP]
refine hasSum_le (fun c => ?_) hf hg
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
c : κ
⊢ extend e f 0 c ≤ g c
[PROOFSTEP]
obtain ⟨i, rfl⟩ | h := em (c ∈ Set.range e)
[GOAL]
case inl.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
i : ι
⊢ extend e f 0 (e i) ≤ g (e i)
[PROOFSTEP]
rw [he.extend_apply]
[GOAL]
case inl.intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
i : ι
⊢ f i ≤ g (e i)
[PROOFSTEP]
exact h _
[GOAL]
case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
c : κ
h : ¬c ∈ Set.range e
⊢ extend e f 0 c ≤ g c
[PROOFSTEP]
rw [extend_apply' _ _ _ h]
[GOAL]
case inr
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g✝ : ι → α
a a₁ a₂ : α
g : κ → α
e : ι → κ
he : Injective e
hs : ∀ (c : κ), ¬c ∈ Set.range e → 0 ≤ g c
h✝ : ∀ (i : ι), f i ≤ g (e i)
hf : HasSum (extend e f 0) a₁
hg : HasSum g a₂
c : κ
h : ¬c ∈ Set.range e
⊢ OfNat.ofNat 0 c ≤ g c
[PROOFSTEP]
exact hs _ h
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : HasSum f a
i : ι
hb : ∀ (j : ι), j ≠ i → 0 ≤ f j
⊢ ∀ (i_1 : ι), ¬i_1 ∈ {i} → 0 ≤ f i_1
[PROOFSTEP]
simpa
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
ha₂ : 0 ≤ a₂
h : ∀ (s : Finset ι), ∑ i in s, f i ≤ a₂
⊢ ∑' (i : ι), f i ≤ a₂
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
ha₂ : 0 ≤ a₂
h : ∀ (s : Finset ι), ∑ i in s, f i ≤ a₂
hf : Summable f
⊢ ∑' (i : ι), f i ≤ a₂
[PROOFSTEP]
exact tsum_le_of_sum_le hf h
[GOAL]
case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
ha₂ : 0 ≤ a₂
h : ∀ (s : Finset ι), ∑ i in s, f i ≤ a₂
hf : ¬Summable f
⊢ ∑' (i : ι), f i ≤ a₂
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf]
[GOAL]
case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
ha₂ : 0 ≤ a₂
h : ∀ (s : Finset ι), ∑ i in s, f i ≤ a₂
hf : ¬Summable f
⊢ 0 ≤ a₂
[PROOFSTEP]
exact ha₂
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 0 ≤ g i
⊢ 0 ≤ ∑' (i : ι), g i
[PROOFSTEP]
by_cases hg : Summable g
[GOAL]
case pos
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 0 ≤ g i
hg : Summable g
⊢ 0 ≤ ∑' (i : ι), g i
[PROOFSTEP]
exact hg.hasSum.nonneg h
[GOAL]
case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), 0 ≤ g i
hg : ¬Summable g
⊢ 0 ≤ ∑' (i : ι), g i
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hg]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), f i ≤ 0
⊢ ∑' (i : ι), f i ≤ 0
[PROOFSTEP]
by_cases hf : Summable f
[GOAL]
case pos
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), f i ≤ 0
hf : Summable f
⊢ ∑' (i : ι), f i ≤ 0
[PROOFSTEP]
exact hf.hasSum.nonpos h
[GOAL]
case neg
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
h : ∀ (i : ι), f i ≤ 0
hf : ¬Summable f
⊢ ∑' (i : ι), f i ≤ 0
[PROOFSTEP]
rw [tsum_eq_zero_of_not_summable hf]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
⊢ HasSum f 0 ↔ f = 0
[PROOFSTEP]
refine' ⟨fun hf' => _, _⟩
[GOAL]
case refine'_1
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
hf' : HasSum f 0
⊢ f = 0
[PROOFSTEP]
ext i
[GOAL]
case refine'_1.h
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
hf' : HasSum f 0
i : ι
⊢ f i = OfNat.ofNat 0 i
[PROOFSTEP]
exact (hf i).antisymm' (le_hasSum hf' _ fun j _ => hf j)
[GOAL]
case refine'_2
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ f i
⊢ f = 0 → HasSum f 0
[PROOFSTEP]
rintro rfl
[GOAL]
case refine'_2
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : OrderedAddCommMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
g : ι → α
a a₁ a₂ : α
hf : ∀ (i : ι), 0 ≤ OfNat.ofNat 0 i
⊢ HasSum 0 0
[PROOFSTEP]
exact hasSum_zero
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
h : f ≤ g
hi : f i < g i
hf : HasSum f a₁
hg : HasSum g a₂
⊢ a₁ < a₂
[PROOFSTEP]
have : update f i 0 ≤ update g i 0 := update_le_update_iff.mpr ⟨rfl.le, fun i _ => h i⟩
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
h : f ≤ g
hi : f i < g i
hf : HasSum f a₁
hg : HasSum g a₂
this : update f i 0 ≤ update g i 0
⊢ a₁ < a₂
[PROOFSTEP]
have : 0 - f i + a₁ ≤ 0 - g i + a₂ := hasSum_le this (hf.update i 0) (hg.update i 0)
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i : ι
h : f ≤ g
hi : f i < g i
hf : HasSum f a₁
hg : HasSum g a₂
this✝ : update f i 0 ≤ update g i 0
this : 0 - f i + a₁ ≤ 0 - g i + a₂
⊢ a₁ < a₂
[PROOFSTEP]
simpa only [zero_sub, add_neg_cancel_left] using add_lt_add_of_lt_of_le hi this
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hsum : Summable g
hg : ∀ (i : ι), 0 ≤ g i
i : ι
hi : 0 < g i
⊢ 0 < ∑' (i : ι), g i
[PROOFSTEP]
rw [← tsum_zero]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hsum : Summable g
hg : ∀ (i : ι), 0 ≤ g i
i : ι
hi : 0 < g i
⊢ ∑' (x : ?m.47496), 0 < ∑' (i : ι), g i
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : OrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : TopologicalAddGroup α
inst✝ : OrderClosedTopology α
f g : ι → α
a₁ a₂ : α
i✝ : ι
hsum : Summable g
hg : ∀ (i : ι), 0 ≤ g i
i : ι
hi : 0 < g i
⊢ Type ?u.47494
[PROOFSTEP]
exact tsum_lt_tsum hg hi summable_zero hsum
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
hf : Summable f
⊢ ∑' (i : ι), f i = 0 ↔ ∀ (x : ι), f x = 0
[PROOFSTEP]
rw [← hasSum_zero_iff, hf.hasSum_iff]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝² : CanonicallyOrderedAddMonoid α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
f : ι → α
a : α
hf : Summable f
⊢ ∑' (i : ι), f i ≠ 0 ↔ ∃ x, f x ≠ 0
[PROOFSTEP]
rw [Ne.def, tsum_eq_zero_iff hf, not_forall]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : CompleteSpace α
f : ι → α
s : Set ι := {x | 0 ≤ f x}
h1 : ∀ (x : ↑s), |f ↑x| = f ↑x
h2 : ∀ (x : ↑sᶜ), |f ↑x| = -f ↑x
⊢ ((Summable fun x => |f ↑x|) ∧ Summable fun x => |f ↑x|) ↔ (Summable fun x => f ↑x) ∧ Summable fun x => -f ↑x
[PROOFSTEP]
simp only [h1, h2]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : CompleteSpace α
f : ι → α
s : Set ι := {x | 0 ≤ f x}
h1 : ∀ (x : ↑s), |f ↑x| = f ↑x
h2 : ∀ (x : ↑sᶜ), |f ↑x| = -f ↑x
⊢ ((Summable fun x => f ↑x) ∧ Summable fun x => -f ↑x) ↔ Summable f
[PROOFSTEP]
simp only [summable_neg_iff, summable_subtype_and_compl]
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
⊢ Finite ι
[PROOFSTEP]
have H : ∀ s : Finset ι, s.card • b ≤ ∑' _ : ι, b := fun s => by
  simpa using sum_le_hasSum s (fun a _ => hb.le) hf.hasSum
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
s : Finset ι
⊢ card s • b ≤ ∑' (x : ι), b
[PROOFSTEP]
simpa using sum_le_hasSum s (fun a _ => hb.le) hf.hasSum
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
⊢ Finite ι
[PROOFSTEP]
obtain ⟨n, hn⟩ := Archimedean.arch (∑' _ : ι, b) hb
[GOAL]
case intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
⊢ Finite ι
[PROOFSTEP]
have : ∀ s : Finset ι, s.card ≤ n := fun s => by simpa [nsmul_le_nsmul_iff hb] using (H s).trans hn
[GOAL]
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
s : Finset ι
⊢ card s ≤ n
[PROOFSTEP]
simpa [nsmul_le_nsmul_iff hb] using (H s).trans hn
[GOAL]
case intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
this : ∀ (s : Finset ι), card s ≤ n
⊢ Finite ι
[PROOFSTEP]
have : Fintype ι := fintypeOfFinsetCardLe n this
[GOAL]
case intro
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝³ : LinearOrderedAddCommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : Archimedean α
inst✝ : OrderClosedTopology α
b : α
hb : 0 < b
hf : Summable fun x => b
H : ∀ (s : Finset ι), card s • b ≤ ∑' (x : ι), b
n : ℕ
hn : ∑' (x : ι), b ≤ n • b
this✝ : ∀ (s : Finset ι), card s ≤ n
this : Fintype ι
⊢ Finite ι
[PROOFSTEP]
infer_instance