LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation.valuation_limit_le_of_tendsto_of_eventually_le
A non-strict valuation bound passes to the limit, including radius zero.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace LocalFieldTheory.DiscreteValuationField.MultiplicativeIntegerValuation
open Filter
open scoped Topology
variable {K : Type*} [Field K]Lean source · statement
theorem valuation_limit_le_of_tendsto_of_eventually_le
(v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
{γ : WithZero (Multiplicative ℤ)} {u : ℕ → K} {z : K}
(hu : Tendsto u atTop (@nhds K (Valued.mk' v).toUniformSpace.toTopologicalSpace z))
(hsmall : ∀ᶠ n : ℕ in atTop, v (u n) ≤ γ) : v z ≤ γ