internlm/Lean-Github huggingface dataset:
Theorem: IsPathConnected.of_frontier
Proof state before:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : ¬x < w
⊢ f (p.extend w) ∈ s
Tactic:
simp only [not_lt] at xw
Proof state after:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : w ≤ x
⊢ f (p.extend w) ∈ s
Theorem: IsPathConnected.of_frontier
Proof state before:
case neg
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
w : ℝ
ws : w < z
xw : w ≤ x
⊢ f (p.extend w) ∈ s
Tactic:
exact lo _ (_root_.trans xw xt.le)
Proof state after:
no goals
Theorem: IsPathConnected.of_frontier
Proof state before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
⊢ p ⟨t, m⟩ = p.extend t
Tactic:
simp only [Path.extend, IccExtend_apply, min_eq_right m.2, max_eq_right m.1]
Proof state after:
no goals
Theorem: IsPathConnected.of_frontier
Proof state before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x✝ : X
fx : f x✝ ∈ s
p : Path x✝ b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
h✝¹ : f (p.extend t) ∈ interior s
o : IsOpen (f ∘ p.extend ⁻¹' interior s)
x y : ℝ
xt : x < t
ty : t < y
h✝ : ∀ (x_1 : ℝ), x < x_1 → x_1 < y → f (p.extend x_1) ∈ interior s
z : ℝ
tz : t < z
zy1 : z < min y 1
zy : z < y
z1 : z < 1
h : z ∈ u
⊢ False
Tactic:
linarith [le_csSup bdd h]
Proof state after:
no goals
Theorem: IsPathConnected.of_frontier
Proof state before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
⊢ Continuous q
Tactic:
rw [← hq]
Proof state after:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
⊢ Continuous fun a => p.extend (min (↑a) t)
Theorem: IsPathConnected.of_frontier
Proof state before:
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
⊢ Continuous fun a => p.extend (min (↑a) t)
Tactic:
exact p.continuous_extend.comp (continuous_subtype_val.min continuous_const)
Proof state after:
no goals
Theorem: IsPathConnected.of_frontier
Proof state before:
case neg.refine_1
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ { toFun := q, continuous_toFun := qc }.toFun 0 = x
Tactic:
simp only [← hq]
Proof state after:
case neg.refine_1
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ p.extend (min (↑0) t) = x
Theorem: IsPathConnected.of_frontier
Proof state before:
case neg.refine_1
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ p.extend (min (↑0) t) = x
Tactic:
simp only [Icc.coe_zero, min_eq_left m.1, p.extend_zero]
Proof state after:
no goals
Theorem: IsPathConnected.of_frontier
Proof state before:
case neg.refine_2
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ { toFun := q, continuous_toFun := qc }.toFun 1 = p ⟨t, m⟩
Tactic:
simp only [← hq]
Proof state after:
case neg.refine_2
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ p.extend (min (↑1) t) = p ⟨t, m⟩
Theorem: IsPathConnected.of_frontier
Proof state before:
case neg.refine_2
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ p.extend (min (↑1) t) = p ⟨t, m⟩
Tactic:
simp only [Icc.coe_one, min_eq_right m.2, Path.extend, IccExtend_apply, max_eq_right m.1]
Proof state after:
no goals
Theorem: IsPathConnected.of_frontier
Proof state before:
case neg.refine_3
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
⊢ ∀ (t_1 : ↑unitInterval), { toFun := q, continuous_toFun := qc, source' := ⋯, target' := ⋯ } t_1 ∈ f ⁻¹' s
Tactic:
intro ⟨a, n⟩
Proof state after:
case neg.refine_3
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
a : ℝ
n : a ∈ unitInterval
⊢ { toFun := q, continuous_toFun := qc, source' := ⋯, target' := ⋯ } ⟨a, n⟩ ∈ f ⁻¹' s
Theorem: IsPathConnected.of_frontier
Proof state before:
case neg.refine_3
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
a : ℝ
n : a ∈ unitInterval
⊢ { toFun := q, continuous_toFun := qc, source' := ⋯, target' := ⋯ } ⟨a, n⟩ ∈ f ⁻¹' s
Tactic:
simp only [mem_preimage, Path.coe_mk_mk, ← hq, Subtype.coe_mk]
Proof state after:
case neg.refine_3
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
a : ℝ
n : a ∈ unitInterval
⊢ f (p.extend (min a t)) ∈ s
Theorem: IsPathConnected.of_frontier
Proof state before:
case neg.refine_3
X✝ : Type
inst✝⁷ : TopologicalSpace X✝
I : Type
inst✝⁶ : TopologicalSpace I
inst✝⁵ : ConditionallyCompleteLinearOrder I
inst✝⁴ : DenselyOrdered I
inst✝³ : OrderTopology I
X Y : Type
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : PathConnectedSpace X
f : X → Y
s : Set Y
pc : IsPathConnected (f ⁻¹' frontier s)
fc : Continuous f
sc : IsClosed s
b : X
fb : f b ∈ frontier s
j : ∀ {y : X}, f y ∈ frontier s → JoinedIn (f ⁻¹' frontier s) b y
bs : f b ∈ s
x : X
fx : f x ∈ s
p : Path x b
u : Set ℝ
hu : Icc 0 1 ∩ ⋂ a, ⋂ (_ : f (p.extend a) ∉ s), Iic a = u
bdd : BddAbove u
un : u.Nonempty
uc : IsClosed u
t : ℝ
ht : sSup u = t
tu : t ∈ u
m : t ∈ Icc 0 1
lo : ∀ a ≤ t, f (p.extend a) ∈ s
t1 : t < 1
ft : f (p ⟨t, m⟩) ∈ frontier s
q : ↑unitInterval → X
hq : (fun a => p.extend (min (↑a) t)) = q
qc : Continuous q
a : ℝ
n : a ∈ unitInterval
⊢ f (p.extend (min a t)) ∈ s
Tactic:
exact lo _ (min_le_right _ _)
Proof state after:
no goals
Theorem: log_log_mono
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 1 < x
xy : x ≤ y
⊢ 0 < x
Tactic:
positivity
Proof state after:
no goals
Theorem: log_neg_log_strict_anti
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 < x
y0 : 0 < y
x1 : x < 1
y1 : y < 1
⊢ (-y.log).log < (-x.log).log ↔ x < y
Tactic:
have lx := neg_pos.mpr (Real.log_neg x0 x1)
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 < x
y0 : 0 < y
x1 : x < 1
y1 : y < 1
lx : 0 < -x.log
⊢ (-y.log).log < (-x.log).log ↔ x < y
Theorem: log_neg_log_strict_anti
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 < x
y0 : 0 < y
x1 : x < 1
y1 : y < 1
lx : 0 < -x.log
⊢ (-y.log).log < (-x.log).log ↔ x < y
Tactic:
have ly := neg_pos.mpr (Real.log_neg y0 y1)
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 < x
y0 : 0 < y
x1 : x < 1
y1 : y < 1
lx : 0 < -x.log
ly : 0 < -y.log
⊢ (-y.log).log < (-x.log).log ↔ x < y
Theorem: log_neg_log_strict_anti
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x y : ℝ
x0 : 0 < x
y0 : 0 < y
x1 : x < 1
y1 : y < 1
lx : 0 < -x.log
ly : 0 < -y.log
⊢ (-y.log).log < (-x.log).log ↔ x < y
Tactic:
rw [Real.log_lt_log_iff ly lx, neg_lt_neg_iff, Real.log_lt_log_iff x0 y0]
Proof state after:
no goals
Theorem: le_log_one_add
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
⊢ log 2 * x ≤ (1 + x).log
Tactic:
rw [Real.le_log_iff_exp_le (by linarith)]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
⊢ (log 2 * x).exp ≤ 1 + x
Theorem: le_log_one_add
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
⊢ (log 2 * x).exp ≤ 1 + x
Tactic:
have x0' : 0 ≤ 1 - x := by linarith
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
⊢ (log 2 * x).exp ≤ 1 + x
Theorem: le_log_one_add
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
⊢ (log 2 * x).exp ≤ 1 + x
Tactic:
have h := convexOn_exp.2 (mem_univ 0) (mem_univ (log 2)) x0' x0 (by abel)
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
h : ((1 - x) • 0 + x • log 2).exp ≤ (1 - x) • exp 0 + x • (log 2).exp
⊢ (log 2 * x).exp ≤ 1 + x
Theorem: le_log_one_add
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
h : ((1 - x) • 0 + x • log 2).exp ≤ (1 - x) • exp 0 + x • (log 2).exp
⊢ (log 2 * x).exp ≤ 1 + x
Tactic:
simp only [smul_eq_mul, mul_zero, zero_add, Real.exp_zero, mul_one, Real.exp_log zero_lt_two] at h
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
h : (x * log 2).exp ≤ 1 - x + x * 2
⊢ (log 2 * x).exp ≤ 1 + x
Theorem: le_log_one_add
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
h : (x * log 2).exp ≤ 1 - x + x * 2
⊢ (log 2 * x).exp ≤ 1 + x
Tactic:
ring_nf at h
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
h : (x * log 2).exp ≤ 1 + x
⊢ (log 2 * x).exp ≤ 1 + x
Theorem: le_log_one_add
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
h : (x * log 2).exp ≤ 1 + x
⊢ (log 2 * x).exp ≤ 1 + x
Tactic:
rwa [mul_comm]
Proof state after:
no goals
Theorem: le_log_one_add
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
⊢ 0 < 1 + x
Tactic:
linarith
Proof state after:
no goals
Theorem: le_log_one_add
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
⊢ 0 ≤ 1 - x
Tactic:
linarith
Proof state after:
no goals
Theorem: le_log_one_add
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x : ℝ
x0 : 0 ≤ x
x1 : x ≤ 1
x0' : 0 ≤ 1 - x
⊢ 1 - x + x = 1
Tactic:
abel
Proof state after:
no goals
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ MonotoneOn (fun x => (x - 1).log / x.log) (Ici 2)
Tactic:
have hd : ∀ x, 2 ≤ x → HasDerivAt (fun x ↦ log (x-1) / log x)
    ((1 / (x-1) * log x - log (x-1) * x⁻¹) / (log x)^2) x := by
  intro x x2
  have l0 : 0 < log x := Real.log_pos (by linarith)
  refine HasDerivAt.div ?_ (Real.hasDerivAt_log (by positivity)) l0.ne'
  exact HasDerivAt.log ((hasDerivAt_id _).sub_const _) (by linarith)
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
⊢ MonotoneOn (fun x => (x - 1).log / x.log) (Ici 2)
Theorem: log_ratio_mono
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
⊢ MonotoneOn (fun x => (x - 1).log / x.log) (Ici 2)
Tactic:
have d : DifferentiableOn ℝ (fun x ↦ log (x-1) / log x) (Ici 2) :=
  fun x m ↦ (hd x m).differentiableAt.differentiableWithinAt
Proof state after:
c : ℂ
d✝ : ℕ
inst✝ : Fact (2 ≤ d✝)
hd :
  ∀ (x : ℝ), 2 ≤ x → HasDerivAt (fun x => (x - 1).log / x.log) ((1 / (x - 1) * x.log - (x - 1).log * x⁻¹) / x.log ^ 2) x
d : DifferentiableOn ℝ (fun x => (x - 1).log / x.log) (Ici 2)
⊢ MonotoneOn (fun x => (x - 1).log / x.log) (Ici 2)