internlm/Lean-Github huggingface dataset:
Theorem: le_liminf.simple
Proof state before:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : c ≤ liminf f atTop
d : L
dc : d < c
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ f n
Tactic:
rw [Filter.liminf_eq, le_sSup_iff, upperBounds] at h
Proof state after:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ b ∈ {x | ∀ ⦃a : L⦄, a ∈ {a | ∀ᶠ (n : ℕ) in atTop, a ≤ f n} → a ≤ x}, c ≤ b
d : L
dc : d < c
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ f n
Theorem: le_liminf.simple
Proof state before:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ b ∈ {x | ∀ ⦃a : L⦄, a ∈ {a | ∀ᶠ (n : ℕ) in atTop, a ≤ f n} → a ≤ x}, c ≤ b
d : L
dc : d < c
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ f n
Tactic:
simp only [Filter.eventually_atTop, ge_iff_le, Set.mem_setOf_eq, forall_exists_index] at h
Proof state after:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c d : L
dc : d < c
h : ∀ (b : L), (∀ ⦃a : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a ≤ f b) → a ≤ b) → c ≤ b
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ f n
Theorem: le_liminf.simple
Proof state before:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c d : L
dc : d < c
h : ∀ (b : L), (∀ ⦃a : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a ≤ f b) → a ≤ b) → c ≤ b
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ f n
Tactic:
specialize h d
Proof state after:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c d : L
dc : d < c
h : (∀ ⦃a : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a ≤ f b) → a ≤ d) → c ≤ d
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ f n
Theorem: le_liminf.simple
Proof state before:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c d : L
dc : d < c
h : (∀ ⦃a : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a ≤ f b) → a ≤ d) → c ≤ d
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ f n
Tactic:
contrapose h
Proof state after:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c d : L
dc : d < c
h : ¬∀ᶠ (n : ℕ) in atTop, d ≤ f n
⊢ ¬((∀ ⦃a : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a ≤ f b) → a ≤ d) → c ≤ d)
Theorem: le_liminf.simple
Proof state before:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c d : L
dc : d < c
h : ¬∀ᶠ (n : ℕ) in atTop, d ≤ f n
⊢ ¬((∀ ⦃a : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a ≤ f b) → a ≤ d) → c ≤ d)
Tactic:
simp only [dc, not_forall, not_le, exists_prop, and_true_iff, Filter.eventually_atTop,
  ge_iff_le, not_exists] at h ⊢
Proof state after:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c d : L
dc : d < c
h : ∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ f x_1 < d
⊢ ∀ ⦃a : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a ≤ f b) → a ≤ d
Theorem: le_liminf.simple
Proof state before:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c d : L
dc : d < c
h : ∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ f x_1 < d
⊢ ∀ ⦃a : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a ≤ f b) → a ≤ d
Tactic:
intro a n an
Proof state after:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c d : L
dc : d < c
h : ∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ f x_1 < d
a : L
n : ℕ
an : ∀ (b : ℕ), n ≤ b → a ≤ f b
⊢ a ≤ d
Theorem: le_liminf.simple
Proof state before:
case mp
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c d : L
dc : d < c
h : ∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ f x_1 < d
a : L
n : ℕ
an : ∀ (b : ℕ), n ≤ b → a ≤ f b
⊢ a ≤ d
Tactic:
rcases h n with ⟨m, nm, fmd⟩
Proof state after:
case mp.intro.intro
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c d : L
dc : d < c
h : ∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ f x_1 < d
a : L
n : ℕ
an : ∀ (b : ℕ), n ≤ b → a ≤ f b
m : ℕ
nm : n ≤ m
fmd : f m < d
⊢ a ≤ d
Theorem: le_liminf.simple
Proof state before:
case mp.intro.intro
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c d : L
dc : d < c
h : ∀ (x : ℕ), ∃ x_1, x ≤ x_1 ∧ f x_1 < d
a : L
n : ℕ
an : ∀ (b : ℕ), n ≤ b → a ≤ f b
m : ℕ
nm : n ≤ m
fmd : f m < d
⊢ a ≤ d
Tactic:
exact _root_.trans (an m nm) fmd.le
Proof state after:
no goals
Theorem: le_liminf.simple
Proof state before:
case mpr
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
⊢ (∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n) → c ≤ liminf f atTop
Tactic:
intro h
Proof state after:
case mpr
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
⊢ c ≤ liminf f atTop
Theorem: le_liminf.simple
Proof state before:
case mpr
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
⊢ c ≤ liminf f atTop
Tactic:
rw [Filter.liminf_eq, le_sSup_iff, upperBounds]
Proof state after:
case mpr
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
⊢ ∀ b ∈ {x | ∀ ⦃a : L⦄, a ∈ {a | ∀ᶠ (n : ℕ) in atTop, a ≤ f n} → a ≤ x}, c ≤ b
Theorem: le_liminf.simple
Proof state before:
case mpr
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
⊢ ∀ b ∈ {x | ∀ ⦃a : L⦄, a ∈ {a | ∀ᶠ (n : ℕ) in atTop, a ≤ f n} → a ≤ x}, c ≤ b
Tactic:
simp only [Filter.eventually_atTop, ge_iff_le, Set.mem_setOf_eq, forall_exists_index]
Proof state after:
case mpr
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
⊢ ∀ (b : L), (∀ ⦃a : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a ≤ f b) → a ≤ b) → c ≤ b
Theorem: le_liminf.simple
Proof state before:
case mpr
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
⊢ ∀ (b : L), (∀ ⦃a : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a ≤ f b) → a ≤ b) → c ≤ b
Tactic:
intro a ah
Proof state after:
case mpr
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
a : L
ah : ∀ ⦃a_1 : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a_1 ≤ f b) → a_1 ≤ a
⊢ c ≤ a
Theorem: le_liminf.simple
Proof state before:
case mpr
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
a : L
ah : ∀ ⦃a_1 : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a_1 ≤ f b) → a_1 ≤ a
⊢ c ≤ a
Tactic:
apply le_of_lt_imp_le
Proof state after:
case mpr.h
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
a : L
ah : ∀ ⦃a_1 : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a_1 ≤ f b) → a_1 ≤ a
⊢ ∀ c_1 < c, c_1 ≤ a
Theorem: le_liminf.simple
Proof state before:
case mpr.h
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
a : L
ah : ∀ ⦃a_1 : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a_1 ≤ f b) → a_1 ≤ a
⊢ ∀ c_1 < c, c_1 ≤ a
Tactic:
intro d dc
Proof state after:
case mpr.h
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
a : L
ah : ∀ ⦃a_1 : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a_1 ≤ f b) → a_1 ≤ a
d : L
dc : d < c
⊢ d ≤ a
Theorem: le_liminf.simple
Proof state before:
case mpr.h
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
a : L
ah : ∀ ⦃a_1 : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a_1 ≤ f b) → a_1 ≤ a
d : L
dc : d < c
⊢ d ≤ a
Tactic:
rcases Filter.eventually_atTop.mp (h d dc) with ⟨n, hn⟩
Proof state after:
case mpr.h.intro
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
a : L
ah : ∀ ⦃a_1 : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a_1 ≤ f b) → a_1 ≤ a
d : L
dc : d < c
n : ℕ
hn : ∀ b ≥ n, d ≤ f b
⊢ d ≤ a
Theorem: le_liminf.simple
Proof state before:
case mpr.h.intro
S : Type
inst✝¹⁷ : RCLike S
inst✝¹⁶ : SMulCommClass ℝ S S
T : Type
inst✝¹⁵ : RCLike T
inst✝¹⁴ : SMulCommClass ℝ T T
E : Type
inst✝¹³ : NormedAddCommGroup E
inst✝¹² : CompleteSpace E
inst✝¹¹ : NormedSpace ℝ E
F : Type
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : CompleteSpace F
inst✝⁸ : NormedSpace ℝ F
H : Type
inst✝⁷ : NormedAddCommGroup H
inst✝⁶ : CompleteSpace H
inst✝⁵ : NormedSpace ℂ H
inst✝⁴ : SecondCountableTopology E
inst✝³ : SecondCountableTopology F
inst✝² : SecondCountableTopology H
L : Type
inst✝¹ : CompleteLinearOrder L
inst✝ : DenselyOrdered L
f : ℕ → L
c : L
h : ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
a : L
ah : ∀ ⦃a_1 : L⦄ (x : ℕ), (∀ (b : ℕ), x ≤ b → a_1 ≤ f b) → a_1 ≤ a
d : L
dc : d < c
n : ℕ
hn : ∀ b ≥ n, d ≤ f b
⊢ d ≤ a
Tactic:
exact ah n hn
Proof state after:
no goals