α : Type u_2
β : Type u_1
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}
α : Type u_2
β : Type u_1
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}
nontriviality α
α : Type u_2
β : Type u_1
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}
α : Type u_2
β : Type u_1
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}
let s := { x | ¬ContinuousWithinAt f (Ioi x) x }
α : Type u_2
β : Type u_1
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}
α : Type u_2
β : Type u_1
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}
choose! z hz using this
α : Type u_2
β : Type u_1
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}
α : Type u_2
β : Type u_1
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}
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
no goals
α : Type u_2
β : Type u_1
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}
exact MapsTo.countable_of_injOn (mapsTo_image f s) I fs_count
α : Type u_2
β : Type u_1
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
α : Type u_2
β : Type u_1
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
rintro x (hx : ¬ContinuousWithinAt f (Ioi x) x)
α : Type u_2
β : Type u_1
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
α : Type u_2
β : Type u_1
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
contrapose! hx
case refine'_1
α : Type u_2
β : Type u_1
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

case refine'_2
α : Type u_2
β : Type u_1
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
α : Type u_2
β : Type u_1
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
refine' tendsto_order.2 ⟨fun m hm => _, fun u hu => _⟩
case refine'_2.intro.intro
α : Type u_2
β : Type u_1
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
case refine'_2
α : Type u_2
β : Type u_1
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
rcases hx u hu with ⟨v, xv, fvu⟩
case refine'_2.intro.intro
α : Type u_2
β : Type u_1
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
case refine'_2.intro.intro
α : Type u_2
β : Type u_1
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
have : Ioo x v ∈ 𝓝[>] x := Ioo_mem_nhdsWithin_Ioi ⟨le_refl _, xv⟩
case h
α : Type u_2
β : Type u_1
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
case refine'_2.intro.intro
α : Type u_2
β : Type u_1
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
filter_upwards [this]with y hy
no goals
case h
α : Type u_2
β : Type u_1
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
apply (hf hy.2.le).trans_lt fvu
no goals
case refine'_1
α : Type u_2
β : Type u_1
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
filter_upwards [@self_mem_nhdsWithin _ _ x (Ioi x)] with y hy using hm.trans_le
  (hf (le_of_lt hy))
case H
α : Type u_2
β : Type u_1
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
α : Type u_2
β : Type u_1
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
apply StrictMonoOn.injOn
case H
α : Type u_2
β : Type u_1
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
case H
α : Type u_2
β : Type u_1
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
intro x hx y _ hxy
no goals
case H
α : Type u_2
β : Type u_1
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
calc
  f x < z x := (hz x hx).1
  _ ≤ f y := (hz x hx).2 y hxy
α : Type u_2
β : Type u_1
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)
α : Type u_2
β : Type u_1
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)
apply Set.PairwiseDisjoint.countable_of_Ioo A
case intro.intro
α : Type u_2
β : Type u_1
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))
α : Type u_2
β : Type u_1
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)
rintro _ ⟨y, ys, rfl⟩
no goals
case intro.intro
α : Type u_2
β : Type u_1
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))
simpa only [I.leftInvOn_invFunOn ys] using (hz y ys).1
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
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)
α : Type u_2
β : Type u_1
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))
rintro _ ⟨u, us, rfl⟩ _ ⟨v, vs, rfl⟩ huv
case intro.intro.intro.intro.inr
α : Type u_2
β : Type u_1
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)

α : Type u_2
β : Type u_1
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)
case intro.intro.intro.intro
α : Type u_2
β : Type u_1
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)
wlog hle : u ≤ v generalizing u v
α : Type u_2
β : Type u_1
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)
α : Type u_2
β : Type u_1
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)
have hlt : u < v := hle.lt_of_ne (ne_of_apply_ne _ huv)
α : Type u_2
β : Type u_1
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
α : Type u_2
β : Type u_1
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)
apply disjoint_iff_forall_ne.2
α : Type u_2
β : Type u_1
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
α : Type u_2
β : Type u_1
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
rintro a ha b hb rfl
α : Type u_2
β : Type u_1
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
α : Type u_2
β : Type u_1
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
simp only [I.leftInvOn_invFunOn us, I.leftInvOn_invFunOn vs] at ha hb
no goals
α : Type u_2
β : Type u_1
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
exact lt_irrefl _ ((ha.2.trans_le ((hz u us).2 v hlt)).trans hb.1)
no goals
case intro.intro.intro.intro.inr
α : Type u_2
β : Type u_1
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)
exact (this v vs u us huv.symm (le_of_not_le hle)).symm