internlm/Lean-Github huggingface dataset:
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
⊢ False
Tactic:
have h14 : ii0' < y := by unfold_let ii0'; aesop
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
⊢ False
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6 : m ∈ Set.Ico x y
h7 : m ∈ Set.Ioc ii0' y
⊢ False
Tactic:
have h8 : f m < f z := h5 ⟨(le_max_left _ _).trans_lt h7.1, h7.2⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6 : m ∈ Set.Ico x y
h7 : m ∈ Set.Ioc ii0' y
h8 : f m < f z
⊢ False
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6 : m ∈ Set.Ico x y
h7 : m ∈ Set.Ioc ii0' y
h8 : f m < f z
⊢ False
Tactic:
have h9 : ¬ f m  < f z := not_lt.mpr (hxyz h6)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6 : m ∈ Set.Ico x y
h7 : m ∈ Set.Ioc ii0' y
h8 : f m < f z
h9 : ¬f m < f z
⊢ False
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6 : m ∈ Set.Ico x y
h7 : m ∈ Set.Ioc ii0' y
h8 : f m < f z
h9 : ¬f m < f z
⊢ False
Tactic:
exact h9 h8
Proof state after:
no goals
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
⊢ y ∈ f ⁻¹' Set.Iio (f z)
Tactic:
aesop
Proof state after:
no goals
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h999 : Set.Ioc ii0 y ⊆ Set.Ioc ii0 ii1
⊢ Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
Tactic:
rw [hiiu'] at h999
Proof state after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h999 : Set.Ioc ii0 y ⊆ ii
⊢ Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h999 : Set.Ioc ii0 y ⊆ ii
⊢ Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
Tactic:
exact h999.trans hiis
Proof state after:
no goals
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
⊢ Set.Ioc ii0 y ⊆ Set.Ioc ii0 ii1
Tactic:
intro w hw
Proof state after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ w ∈ Set.Ioc ii0 ii1
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ w ∈ Set.Ioc ii0 ii1
Tactic:
constructor
Proof state after:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ ii0 < w

case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ w ≤ ii1
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ ii0 < w
Tactic:
exact hw.1
Proof state after:
no goals
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ w ≤ ii1
Tactic:
rw [←hiiu'] at hyii
Proof state after:
case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ Set.Ioc ii0 ii1
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ w ≤ ii1
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ Set.Ioc ii0 ii1
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
w : ℝ
hw : w ∈ Set.Ioc ii0 y
⊢ w ≤ ii1
Tactic:
exact hw.2.trans hyii.2
Proof state after:
no goals
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
⊢ ii0' < y
Tactic:
unfold_let ii0'
Proof state after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
⊢ max ii0 x < y
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
⊢ max ii0 x < y
Tactic:
aesop
Proof state after:
no goals
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
⊢ m ∈ Set.Ico x y
Tactic:
constructor
Proof state after:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
⊢ x ≤ m

case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
⊢ m < y
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
⊢ x ≤ m
Tactic:
have h10 : x ≤ ii0' := le_max_right _ _
Proof state after:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h10 : x ≤ ii0'
⊢ x ≤ m
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h10 : x ≤ ii0'
⊢ x ≤ m
Tactic:
have h13 : (x * 2) / 2 ≤ (ii0' + y) / 2 := by linarith
Proof state after:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h10 : x ≤ ii0'
h13 : x * 2 / 2 ≤ (ii0' + y) / 2
⊢ x ≤ m
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h10 : x ≤ ii0'
h13 : x * 2 / 2 ≤ (ii0' + y) / 2
⊢ x ≤ m
Tactic:
rwa [mul_div_cancel_right₀ x two_ne_zero] at h13
Proof state after:
no goals
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h10 : x ≤ ii0'
⊢ x * 2 / 2 ≤ (ii0' + y) / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
⊢ m < y
Tactic:
exact add_div_two_lt_right.mpr h14
Proof state after:
no goals
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6 : m ∈ Set.Ico x y
⊢ m ∈ Set.Ioc ii0' y
Tactic:
cases' h6 with h6l h6r
Proof state after:
case intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6l : x ≤ m
h6r : m < y
⊢ m ∈ Set.Ioc ii0' y
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6l : x ≤ m
h6r : m < y
⊢ m ∈ Set.Ioc ii0' y
Tactic:
constructor
Proof state after:
case intro.left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6l : x ≤ m
h6r : m < y
⊢ ii0' < m

case intro.right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6l : x ≤ m
h6r : m < y
⊢ m ≤ y
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case intro.left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
L1 : ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
x y : ℝ
hxy : x < y
hxyz : Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
hy : y ∉ f ⁻¹' Set.Ici (f z)
h1 : IsOpen (Set.Iio (f z))
h2 : IsOpen (f ⁻¹' Set.Iio (f z))
h3 : y ∈ f ⁻¹' Set.Iio (f z)
ii : Set ℝ
ii0 ii1 : ℝ
hiiu' : Set.Ioc ii0 ii1 = ii
hyii : y ∈ ii
hiis : ii ⊆ f ⁻¹' Set.Iio (f z)
h5 : Set.Ioc ii0 y ⊆ f ⁻¹' Set.Iio (f z)
ii0' : ℝ := max ii0 x
m : ℝ := (ii0' + y) / 2
h14 : ii0' < y
h6l : x ≤ m
h6r : m < y
⊢ ii0' < m
Tactic:
exact left_lt_add_div_two.mpr h14
Proof state after:
no goals