internlm/Lean-Github huggingface dataset:
Theorem: AnalyticOn.maxLog_norm_subharmonicOn
Proof state before:
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
f : ℂ → H
s : Set ℂ
fa : AnalyticOn ℂ f s
b✝ : ℝ
gc : ContinuousOn (fun z => maxLog b✝ ‖f z‖) s
ft : ∀ z ∈ s, Tendsto (⇑(partialSups fun k => maxLog b✝ ‖(duals k) (f z)‖)) atTop (𝓝 (maxLog b✝ ‖f z‖))
fs : ∀ (n : ℕ), SubharmonicOn (fun z => (partialSups fun k => maxLog b✝ ‖(duals k) (f z)‖) n) s
a b : ℕ
ab : a ≤ b
z : ℂ
⊢ (partialSups fun k => maxLog b✝ (Complex.abs ((duals k) (f z)))) a ≤
    (partialSups fun k => maxLog b✝ (Complex.abs ((duals k) (f z)))) b
Tactic:
apply (partialSups _).monotone ab
Proof state after:
no goals
Theorem: Limsup.neg
Proof state before:
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
f : ℕ → ℝ
⊢ limsup (fun n => f n) atTop = -liminf (fun n => -f n) atTop
Tactic:
rw [Filter.limsup_eq]
Proof state after:
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
f : ℕ → ℝ
⊢ sInf {a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a} = -liminf (fun n => -f n) atTop
Theorem: Limsup.neg
Proof state before:
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
f : ℕ → ℝ
⊢ sInf {a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a} = -liminf (fun n => -f n) atTop
Tactic:
rw [Filter.liminf_eq]
Proof state after:
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
f : ℕ → ℝ
⊢ sInf {a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a} = -sSup {a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n}
Theorem: Limsup.neg
Proof state before:
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
f : ℕ → ℝ
⊢ sInf {a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a} = -sSup {a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n}
Tactic:
rw [Real.sInf_def]
Proof state after:
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
f : ℕ → ℝ
⊢ -sSup (-{a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a}) = -sSup {a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n}
Theorem: Limsup.neg
Proof state before:
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
f : ℕ → ℝ
⊢ -sSup (-{a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a}) = -sSup {a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n}
Tactic:
have ns : -{a | ∀ᶠ n in atTop, a ≤ -f n} = {a | ∀ᶠ n in atTop, f n ≤ a} := by
  apply Set.ext
  simp only [Set.mem_neg, Set.mem_setOf_eq, neg_le_neg_iff, iff_self_iff, forall_const]
Proof state after:
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
f : ℕ → ℝ
ns : -{a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n} = {a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a}
⊢ -sSup (-{a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a}) = -sSup {a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n}
Theorem: Limsup.neg
Proof state before:
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
f : ℕ → ℝ
ns : -{a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n} = {a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a}
⊢ -sSup (-{a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a}) = -sSup {a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n}
Tactic:
simp_rw [← ns]
Proof state after:
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
f : ℕ → ℝ
ns : -{a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n} = {a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a}
⊢ -sSup (- -{a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n}) = -sSup {a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n}
Theorem: Limsup.neg
Proof state before:
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
f : ℕ → ℝ
ns : -{a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n} = {a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a}
⊢ -sSup (- -{a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n}) = -sSup {a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n}
Tactic:
simp only [neg_neg]
Proof state after:
no goals
Theorem: Limsup.neg
Proof state before:
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
f : ℕ → ℝ
⊢ -{a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n} = {a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a}
Tactic:
apply Set.ext
Proof state after:
case 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
f : ℕ → ℝ
⊢ ∀ (x : ℝ), x ∈ -{a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n} ↔ x ∈ {a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a}
Theorem: Limsup.neg
Proof state before:
case 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
f : ℕ → ℝ
⊢ ∀ (x : ℝ), x ∈ -{a | ∀ᶠ (n : ℕ) in atTop, a ≤ -f n} ↔ x ∈ {a | ∀ᶠ (n : ℕ) in atTop, f n ≤ a}
Tactic:
simp only [Set.mem_neg, Set.mem_setOf_eq, neg_le_neg_iff, iff_self_iff, forall_const]
Proof state after:
no goals
Theorem: ENNReal.induction
Proof state before:
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
p : ℝ≥0∞ → Prop
pi : p ⊤
pf : ∀ (x : ℝ), 0 ≤ x → p (ENNReal.ofReal x)
⊢ ∀ (e : ℝ≥0∞), p e
Tactic:
rw [ENNReal.forall_ennreal]
Proof state after:
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
p : ℝ≥0∞ → Prop
pi : p ⊤
pf : ∀ (x : ℝ), 0 ≤ x → p (ENNReal.ofReal x)
⊢ (∀ (r : ℝ≥0), p ↑r) ∧ p ⊤
Theorem: ENNReal.induction
Proof state before:
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
p : ℝ≥0∞ → Prop
pi : p ⊤
pf : ∀ (x : ℝ), 0 ≤ x → p (ENNReal.ofReal x)
⊢ (∀ (r : ℝ≥0), p ↑r) ∧ p ⊤
Tactic:
refine ⟨?_, pi⟩
Proof state after:
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
p : ℝ≥0∞ → Prop
pi : p ⊤
pf : ∀ (x : ℝ), 0 ≤ x → p (ENNReal.ofReal x)
⊢ ∀ (r : ℝ≥0), p ↑r
Theorem: ENNReal.induction
Proof state before:
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
p : ℝ≥0∞ → Prop
pi : p ⊤
pf : ∀ (x : ℝ), 0 ≤ x → p (ENNReal.ofReal x)
⊢ ∀ (r : ℝ≥0), p ↑r
Tactic:
rw [NNReal.forall]
Proof state after:
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
p : ℝ≥0∞ → Prop
pi : p ⊤
pf : ∀ (x : ℝ), 0 ≤ x → p (ENNReal.ofReal x)
⊢ ∀ (x : ℝ) (hx : 0 ≤ x), p ↑⟨x, hx⟩
Theorem: ENNReal.induction
Proof state before:
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
p : ℝ≥0∞ → Prop
pi : p ⊤
pf : ∀ (x : ℝ), 0 ≤ x → p (ENNReal.ofReal x)
⊢ ∀ (x : ℝ) (hx : 0 ≤ x), p ↑⟨x, hx⟩
Tactic:
simpa only [← ENNReal.ofReal_eq_coe_nnreal]
Proof state after:
no goals
Theorem: le_of_lt_imp_le
Proof state before:
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✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : ∀ c < a, c ≤ b
⊢ a ≤ b
Tactic:
contrapose h
Proof state after:
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✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : ¬a ≤ b
⊢ ¬∀ c < a, c ≤ b
Theorem: le_of_lt_imp_le
Proof state before:
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✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : ¬a ≤ b
⊢ ¬∀ c < a, c ≤ b
Tactic:
simp only [not_forall, not_le, exists_prop] at h ⊢
Proof state after:
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✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : b < a
⊢ ∃ x < a, b < x
Theorem: le_of_lt_imp_le
Proof state before:
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✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : b < a
⊢ ∃ x < a, b < x
Tactic:
rcases exists_between h with ⟨x, bx, xa⟩
Proof state after:
case 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✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : b < a
x : L
bx : b < x
xa : x < a
⊢ ∃ x < a, b < x
Theorem: le_of_lt_imp_le
Proof state before:
case 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✝¹ : LinearOrder L
inst✝ : DenselyOrdered L
a b : L
h : b < a
x : L
bx : b < x
xa : x < a
⊢ ∃ x < a, b < x
Tactic:
exact ⟨x, xa, bx⟩
Proof state after:
no goals
Theorem: le_liminf.simple
Proof state before:
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
⊢ c ≤ liminf f atTop ↔ ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
Tactic:
constructor
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
⊢ c ≤ liminf f atTop → ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n

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
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
⊢ c ≤ liminf f atTop → ∀ d < c, ∀ᶠ (n : ℕ) in atTop, d ≤ f n
Tactic:
intro h d dc
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 : c ≤ liminf f atTop
d : L
dc : d < c
⊢ ∀ᶠ (n : ℕ) in atTop, d ≤ f n