internlm/Lean-Github huggingface dataset:
Theorem: UpperLowerContinuous.infinite_interval_lower_open
Proof state before:
case h.right.left
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a ∈ Set.Ico a (a + 1)
Tactic:
constructor
Proof state after:
case h.right.left.left
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a ≤ a

case h.right.left.right
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a < a + 1
Theorem: UpperLowerContinuous.infinite_interval_lower_open
Proof state before:
case h.right.left.left
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a ≤ a
Tactic:
exact Eq.le rfl
Proof state after:
no goals
Theorem: UpperLowerContinuous.infinite_interval_lower_open
Proof state before:
case h.right.left.right
x a : ℝ
ha : a ∈ Set.Ici x
⊢ a < a + 1
Tactic:
exact lt_add_one a
Proof state after:
no goals
Theorem: UpperLowerContinuous.infinite_interval_lower_open
Proof state before:
case h.right.right
x a : ℝ
ha : a ∈ Set.Ici x
⊢ Set.Ico a (a + 1) ⊆ Set.Ici x
Tactic:
intro y hy
Proof state after:
case h.right.right
x a : ℝ
ha : a ∈ Set.Ici x
y : ℝ
hy : y ∈ Set.Ico a (a + 1)
⊢ y ∈ Set.Ici x
Theorem: UpperLowerContinuous.infinite_interval_lower_open
Proof state before:
case h.right.right
x a : ℝ
ha : a ∈ Set.Ici x
y : ℝ
hy : y ∈ Set.Ico a (a + 1)
⊢ y ∈ Set.Ici x
Tactic:
rw[Set.mem_Ici] at ha
Proof state after:
case h.right.right
x a : ℝ
ha : x ≤ a
y : ℝ
hy : y ∈ Set.Ico a (a + 1)
⊢ y ∈ Set.Ici x
Theorem: UpperLowerContinuous.infinite_interval_lower_open
Proof state before:
case h.right.right
x a : ℝ
ha : x ≤ a
y : ℝ
hy : y ∈ Set.Ico a (a + 1)
⊢ y ∈ Set.Ici x
Tactic:
exact ha.trans hy.1
Proof state after:
no goals
Theorem: UpperLowerContinuous.infinite_interval_upper_open
Proof state before:
x : ℝ
⊢ IsOpen (Set.Iio x)
Tactic:
rw [@TopologicalSpace.IsTopologicalBasis.isOpen_iff
        ℝ tᵤ _ upper_intervals upper_basis]
Proof state after:
x : ℝ
⊢ ∀ a ∈ Set.Iio x, ∃ t ∈ upper_intervals, a ∈ t ∧ t ⊆ Set.Iio x
Theorem: UpperLowerContinuous.infinite_interval_upper_open
Proof state before:
x : ℝ
⊢ ∀ a ∈ Set.Iio x, ∃ t ∈ upper_intervals, a ∈ t ∧ t ⊆ Set.Iio x
Tactic:
intro a ha
Proof state after:
x a : ℝ
ha : a ∈ Set.Iio x
⊢ ∃ t ∈ upper_intervals, a ∈ t ∧ t ⊆ Set.Iio x
Theorem: UpperLowerContinuous.infinite_interval_upper_open
Proof state before:
x a : ℝ
ha : a ∈ Set.Iio x
⊢ ∃ t ∈ upper_intervals, a ∈ t ∧ t ⊆ Set.Iio x
Tactic:
use Set.Ioc (a - 1) a
Proof state after:
case h
x a : ℝ
ha : a ∈ Set.Iio x
⊢ Set.Ioc (a - 1) a ∈ upper_intervals ∧ a ∈ Set.Ioc (a - 1) a ∧ Set.Ioc (a - 1) a ⊆ Set.Iio x
Theorem: UpperLowerContinuous.infinite_interval_upper_open
Proof state before:
case h
x a : ℝ
ha : a ∈ Set.Iio x
⊢ Set.Ioc (a - 1) a ∈ upper_intervals ∧ a ∈ Set.Ioc (a - 1) a ∧ Set.Ioc (a - 1) a ⊆ Set.Iio x
Tactic:
constructor
Proof state after:
case h.left
x a : ℝ
ha : a ∈ Set.Iio x
⊢ Set.Ioc (a - 1) a ∈ upper_intervals

case h.right
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ∈ Set.Ioc (a - 1) a ∧ Set.Ioc (a - 1) a ⊆ Set.Iio x
Theorem: UpperLowerContinuous.infinite_interval_upper_open
Proof state before:
case h.left
x a : ℝ
ha : a ∈ Set.Iio x
⊢ Set.Ioc (a - 1) a ∈ upper_intervals
Tactic:
exact ⟨a - 1, a, rfl⟩
Proof state after:
no goals
Theorem: UpperLowerContinuous.infinite_interval_upper_open
Proof state before:
case h.right
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ∈ Set.Ioc (a - 1) a ∧ Set.Ioc (a - 1) a ⊆ Set.Iio x
Tactic:
constructor
Proof state after:
case h.right.left
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ∈ Set.Ioc (a - 1) a

case h.right.right
x a : ℝ
ha : a ∈ Set.Iio x
⊢ Set.Ioc (a - 1) a ⊆ Set.Iio x
Theorem: UpperLowerContinuous.infinite_interval_upper_open
Proof state before:
case h.right.left
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ∈ Set.Ioc (a - 1) a
Tactic:
constructor
Proof state after:
case h.right.left.left
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a - 1 < a

case h.right.left.right
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ≤ a
Theorem: UpperLowerContinuous.infinite_interval_upper_open
Proof state before:
case h.right.left.left
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a - 1 < a
Tactic:
simp only [Set.mem_Iio, sub_lt_self_iff, zero_lt_one]
Proof state after:
no goals
Theorem: UpperLowerContinuous.infinite_interval_upper_open
Proof state before:
case h.right.left.right
x a : ℝ
ha : a ∈ Set.Iio x
⊢ a ≤ a
Tactic:
exact Eq.le rfl
Proof state after:
no goals
Theorem: UpperLowerContinuous.infinite_interval_upper_open
Proof state before:
case h.right.right
x a : ℝ
ha : a ∈ Set.Iio x
⊢ Set.Ioc (a - 1) a ⊆ Set.Iio x
Tactic:
intro y hy
Proof state after:
case h.right.right
x a : ℝ
ha : a ∈ Set.Iio x
y : ℝ
hy : y ∈ Set.Ioc (a - 1) a
⊢ y ∈ Set.Iio x
Theorem: UpperLowerContinuous.infinite_interval_upper_open
Proof state before:
case h.right.right
x a : ℝ
ha : a ∈ Set.Iio x
y : ℝ
hy : y ∈ Set.Ioc (a - 1) a
⊢ y ∈ Set.Iio x
Tactic:
exact hy.2.trans_lt ha
Proof state after:
no goals
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
⊢ Monotone f
Tactic:
intro z b hz
Proof state after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
⊢ f z ≤ f b
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)
L2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) → y ∈ f ⁻¹' Set.Ici (f z)
⊢ f z ≤ f b
Tactic:
have h0 : Set.Ici z ⊆ f ⁻¹' (Set.Ici (f z)) :=
  real_induction L1 L2 (@Set.left_mem_Ici _ _ (f z))
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)
L2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) → y ∈ f ⁻¹' Set.Ici (f z)
h0 : Set.Ici z ⊆ f ⁻¹' Set.Ici (f z)
⊢ f z ≤ f b
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)
L2 : ∀ (x y : ℝ), x < y → Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) → y ∈ f ⁻¹' Set.Ici (f z)
h0 : Set.Ici z ⊆ f ⁻¹' Set.Ici (f z)
⊢ f z ≤ f b
Tactic:
exact h0 hz
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
⊢ ∀ x ∈ f ⁻¹' Set.Ici (f z), ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
Tactic:
intro x hx
Proof state after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
Tactic:
have inverse_image_open := continuous_def.mp hlc _ (infinite_interval_lower_open (f z))
Proof state after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
Tactic:
have h2 := (@TopologicalSpace.IsTopologicalBasis.isOpen_iff ℝ tₗ (f ⁻¹' (Set.Ici (f z)))
   lower_intervals lower_basis).mp inverse_image_open x hx
Proof state after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
h2 : ∃ t ∈ lower_intervals, x ∈ t ∧ t ⊆ f ⁻¹' Set.Ici (f z)
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
h2 : ∃ t ∈ lower_intervals, x ∈ t ∧ t ⊆ f ⁻¹' Set.Ici (f z)
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
Tactic:
obtain ⟨t , ⟨ta, tb, htb⟩, xint, tsub⟩ := h2
Proof state after:
case intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case intro.intro.intro.intro.intro
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z)
Tactic:
use tb
Proof state after:
case h
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ x < tb ∧ Set.Ico x tb ⊆ f ⁻¹' Set.Ici (f z)
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case h
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ x < tb ∧ Set.Ico x tb ⊆ f ⁻¹' Set.Ici (f z)
Tactic:
constructor
Proof state after:
case h.left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ x < tb

case h.right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ Set.Ico x tb ⊆ f ⁻¹' Set.Ici (f z)
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case h.left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ x < tb
Tactic:
rw [←htb] at xint
Proof state after:
case h.left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ x < tb
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case h.left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ x < tb
Tactic:
exact xint.2
Proof state after:
no goals
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case h.right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
auxsub : Set.Ico x tb ⊆ t
⊢ Set.Ico x tb ⊆ f ⁻¹' Set.Ici (f z)
Tactic:
exact auxsub.trans tsub
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
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
⊢ Set.Ico x tb ⊆ t
Tactic:
intro xx hxx
Proof state after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx ∈ t
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx ∈ t
Tactic:
rw[←htb]
Proof state after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx ∈ Set.Ico ta tb
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ t
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx ∈ Set.Ico ta tb
Tactic:
rw[←htb] at xint
Proof state after:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx ∈ Set.Ico ta tb
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx ∈ Set.Ico ta tb
Tactic:
constructor
Proof state after:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ ta ≤ xx

case right
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx < tb
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case left
f : ℝ → ℝ
huc : Continuous f
hlc : Continuous f
z b : ℝ
hz : z ≤ b
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ ta ≤ xx
Tactic:
exact xint.1.trans hxx.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
x : ℝ
hx : x ∈ f ⁻¹' Set.Ici (f z)
inverse_image_open : IsOpen (f ⁻¹' Set.Ici (f z))
t : Set ℝ
ta tb : ℝ
htb : Set.Ico ta tb = t
xint : x ∈ Set.Ico ta tb
tsub : t ⊆ f ⁻¹' Set.Ici (f z)
xx : ℝ
hxx : xx ∈ Set.Ico x tb
⊢ xx < tb
Tactic:
exact hxx.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 : ℝ), x < y → Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) → y ∈ f ⁻¹' Set.Ici (f z)
Tactic:
intro x
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 : ℝ), x < y → Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) → y ∈ f ⁻¹' Set.Ici (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 : ℝ), x < y → Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) → y ∈ f ⁻¹' Set.Ici (f z)
Tactic:
by_contra! H
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 : ℝ
H : ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) ∧ y ∉ f ⁻¹' Set.Ici (f z)
⊢ False
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 : ℝ
H : ∃ y, x < y ∧ Set.Ico x y ⊆ f ⁻¹' Set.Ici (f z) ∧ y ∉ f ⁻¹' Set.Ici (f z)
⊢ False
Tactic:
obtain ⟨y, hxy, hxyz, hy⟩ := H
Proof state after:
case 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)
⊢ False
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case 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)
⊢ False
Tactic:
have h1 := infinite_interval_upper_open (f z)
Proof state after:
case 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))
⊢ False
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case 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))
⊢ False
Tactic:
have h2 := continuous_def.mp huc (Set.Iio (f z)) h1
Proof state after:
case 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))
⊢ False
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case 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))
⊢ False
Tactic:
have h3 : y ∈ f ⁻¹' Set.Iio (f z) := by aesop
Proof state after:
case 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)
⊢ False
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case 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)
⊢ False
Tactic:
have h4 := (@TopologicalSpace.IsTopologicalBasis.isOpen_iff
             ℝ tᵤ _ upper_intervals upper_basis).mp h2 y h3
Proof state after:
case 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)
h4 : ∃ t ∈ upper_intervals, y ∈ t ∧ t ⊆ f ⁻¹' Set.Iio (f z)
⊢ False
Theorem: UpperLowerContinuous.monotone_of_upper_lower_continuous
Proof state before:
case 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)
h4 : ∃ t ∈ upper_intervals, y ∈ t ∧ t ⊆ f ⁻¹' Set.Iio (f z)
⊢ False
Tactic:
obtain ⟨ii, ⟨ii0, ii1, hiiu'⟩, hyii, hiis⟩ := h4
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)
⊢ 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)
⊢ False
Tactic:
let ii0' := max ii0 x
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
⊢ 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
⊢ False
Tactic:
let m := (ii0' + y) / 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
⊢ False