HepLean Documentation

Mathlib.Order.Filter.AtTopBot.Archimedean

Filter.atTop filter and archimedean (semi)rings/fields #

In this file we prove that for a linear ordered archimedean semiring R and a function f : α → ℕ, the function Nat.cast ∘ f : α → R tends to Filter.atTop along a filter l if and only if so does f. We also prove that Nat.cast : ℕ → R tends to Filter.atTop along Filter.atTop, as well as version of these two results for ℤ (and a ring R) and ℚ (and a field R).

source
@[simp]
theorem Nat.comap_cast_atTop {R : Type u_2} [StrictOrderedSemiring R] [Archimedean R] :
Filter.comap Nat.cast Filter.atTop = Filter.atTop
source
theorem tendsto_natCast_atTop_iff {α : Type u_1} {R : Type u_2} [StrictOrderedSemiring R] [Archimedean R] {f : α → ℕ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
source
@[deprecated tendsto_natCast_atTop_iff]
theorem tendsto_nat_cast_atTop_iff {α : Type u_1} {R : Type u_2} [StrictOrderedSemiring R] [Archimedean R] {f : α → ℕ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop

Alias of tendsto_natCast_atTop_iff.

source
theorem tendsto_natCast_atTop_atTop {R : Type u_2} [OrderedSemiring R] [Archimedean R] :
Filter.Tendsto Nat.cast Filter.atTop Filter.atTop
source
@[deprecated tendsto_natCast_atTop_atTop]
theorem tendsto_nat_cast_atTop_atTop {R : Type u_2} [OrderedSemiring R] [Archimedean R] :
Filter.Tendsto Nat.cast Filter.atTop Filter.atTop

Alias of tendsto_natCast_atTop_atTop.

source
theorem Filter.Eventually.natCast_atTop {R : Type u_2} [OrderedSemiring R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in Filter.atTop, p x) :
∀ᶠ (n : ℕ) in Filter.atTop, p ↑n
source
@[deprecated Filter.Eventually.natCast_atTop]
theorem Filter.Eventually.nat_cast_atTop {R : Type u_2} [OrderedSemiring R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in Filter.atTop, p x) :
∀ᶠ (n : ℕ) in Filter.atTop, p ↑n

Alias of Filter.Eventually.natCast_atTop.

source
@[simp]
theorem Int.comap_cast_atTop {R : Type u_2} [StrictOrderedRing R] [Archimedean R] :
Filter.comap Int.cast Filter.atTop = Filter.atTop
source
@[simp]
theorem Int.comap_cast_atBot {R : Type u_2} [StrictOrderedRing R] [Archimedean R] :
Filter.comap Int.cast Filter.atBot = Filter.atBot
source
theorem tendsto_intCast_atTop_iff {α : Type u_1} {R : Type u_2} [StrictOrderedRing R] [Archimedean R] {f : α → ℤ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
source
@[deprecated tendsto_intCast_atTop_iff]
theorem tendsto_int_cast_atTop_iff {α : Type u_1} {R : Type u_2} [StrictOrderedRing R] [Archimedean R] {f : α → ℤ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop

Alias of tendsto_intCast_atTop_iff.

source
theorem tendsto_intCast_atBot_iff {α : Type u_1} {R : Type u_2} [StrictOrderedRing R] [Archimedean R] {f : α → ℤ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
source
@[deprecated tendsto_intCast_atBot_iff]
theorem tendsto_int_cast_atBot_iff {α : Type u_1} {R : Type u_2} [StrictOrderedRing R] [Archimedean R] {f : α → ℤ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot

Alias of tendsto_intCast_atBot_iff.

source
theorem tendsto_intCast_atTop_atTop {R : Type u_2} [StrictOrderedRing R] [Archimedean R] :
Filter.Tendsto Int.cast Filter.atTop Filter.atTop
source
@[deprecated tendsto_intCast_atTop_atTop]
theorem tendsto_int_cast_atTop_atTop {R : Type u_2} [StrictOrderedRing R] [Archimedean R] :
Filter.Tendsto Int.cast Filter.atTop Filter.atTop

Alias of tendsto_intCast_atTop_atTop.

source
theorem Filter.Eventually.intCast_atTop {R : Type u_2} [StrictOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in Filter.atTop, p x) :
∀ᶠ (n : ℤ) in Filter.atTop, p ↑n
source
@[deprecated Filter.Eventually.intCast_atTop]
theorem Filter.Eventually.int_cast_atTop {R : Type u_2} [StrictOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in Filter.atTop, p x) :
∀ᶠ (n : ℤ) in Filter.atTop, p ↑n

Alias of Filter.Eventually.intCast_atTop.

source
theorem Filter.Eventually.intCast_atBot {R : Type u_2} [StrictOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in Filter.atBot, p x) :
∀ᶠ (n : ℤ) in Filter.atBot, p ↑n
source
@[deprecated Filter.Eventually.intCast_atBot]
theorem Filter.Eventually.int_cast_atBot {R : Type u_2} [StrictOrderedRing R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in Filter.atBot, p x) :
∀ᶠ (n : ℤ) in Filter.atBot, p ↑n

Alias of Filter.Eventually.intCast_atBot.

source
@[simp]
theorem Rat.comap_cast_atTop {R : Type u_2} [LinearOrderedField R] [Archimedean R] :
Filter.comap Rat.cast Filter.atTop = Filter.atTop
source
@[simp]
theorem Rat.comap_cast_atBot {R : Type u_2} [LinearOrderedField R] [Archimedean R] :
Filter.comap Rat.cast Filter.atBot = Filter.atBot
source
theorem tendsto_ratCast_atTop_iff {α : Type u_1} {R : Type u_2} [LinearOrderedField R] [Archimedean R] {f : α → ℚ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
source
@[deprecated tendsto_ratCast_atTop_iff]
theorem tendsto_rat_cast_atTop_iff {α : Type u_1} {R : Type u_2} [LinearOrderedField R] [Archimedean R] {f : α → ℚ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop

Alias of tendsto_ratCast_atTop_iff.

source
theorem tendsto_ratCast_atBot_iff {α : Type u_1} {R : Type u_2} [LinearOrderedField R] [Archimedean R] {f : α → ℚ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
source
@[deprecated tendsto_ratCast_atBot_iff]
theorem tendsto_rat_cast_atBot_iff {α : Type u_1} {R : Type u_2} [LinearOrderedField R] [Archimedean R] {f : α → ℚ} {l : Filter α} :
Filter.Tendsto (fun (n : α) => ↑(f n)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot

Alias of tendsto_ratCast_atBot_iff.

source
theorem Filter.Eventually.ratCast_atTop {R : Type u_2} [LinearOrderedField R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in Filter.atTop, p x) :
∀ᶠ (n : ℚ) in Filter.atTop, p ↑n
source
@[deprecated Filter.Eventually.ratCast_atTop]
theorem Filter.Eventually.rat_cast_atTop {R : Type u_2} [LinearOrderedField R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in Filter.atTop, p x) :
∀ᶠ (n : ℚ) in Filter.atTop, p ↑n

Alias of Filter.Eventually.ratCast_atTop.

source
theorem Filter.Eventually.ratCast_atBot {R : Type u_2} [LinearOrderedField R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in Filter.atBot, p x) :
∀ᶠ (n : ℚ) in Filter.atBot, p ↑n
source
@[deprecated Filter.Eventually.ratCast_atBot]
theorem Filter.Eventually.rat_cast_atBot {R : Type u_2} [LinearOrderedField R] [Archimedean R] {p : R → Prop} (h : ∀ᶠ (x : R) in Filter.atBot, p x) :
∀ᶠ (n : ℚ) in Filter.atBot, p ↑n

Alias of Filter.Eventually.ratCast_atBot.

source
theorem atTop_hasAntitoneBasis_of_archimedean {R : Type u_2} [OrderedSemiring R] [Archimedean R] :
Filter.atTop.HasAntitoneBasis fun (n : ℕ) => Set.Ici ↑n
source
theorem atTop_hasCountableBasis_of_archimedean {R : Type u_2} [OrderedSemiring R] [Archimedean R] :
Filter.atTop.HasCountableBasis (fun (x : ℕ) => True) fun (n : ℕ) => Set.Ici ↑n
source
theorem atBot_hasCountableBasis_of_archimedean {R : Type u_2} [OrderedRing R] [Archimedean R] :
Filter.atBot.HasCountableBasis (fun (x : ℤ) => True) fun (m : ℤ) => Set.Iic ↑m
source
@[instance 100]
instance atTop_isCountablyGenerated_of_archimedean {R : Type u_2} [OrderedSemiring R] [Archimedean R] :
Filter.atTop.IsCountablyGenerated
Equations
  • ⋯ = ⋯
source
@[instance 100]
instance atBot_isCountablyGenerated_of_archimedean {R : Type u_2} [OrderedRing R] [Archimedean R] :
Filter.atBot.IsCountablyGenerated
Equations
  • ⋯ = ⋯
source
theorem Filter.Tendsto.const_mul_atTop' {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [LinearOrderedSemiring R] [Archimedean R] (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atTop) :
Filter.Tendsto (fun (x : α) => r * f x) l Filter.atTop

If a function tends to infinity along a filter, then this function multiplied by a positive constant (on the left) also tends to infinity. The archimedean assumption is convenient to get a statement that works on ℕ, ℤ and ℝ, although not necessary (a version in ordered fields is given in Filter.Tendsto.const_mul_atTop).

source
theorem Filter.Tendsto.atTop_mul_const' {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [LinearOrderedSemiring R] [Archimedean R] (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atTop) :
Filter.Tendsto (fun (x : α) => f x * r) l Filter.atTop

If a function tends to infinity along a filter, then this function multiplied by a positive constant (on the right) also tends to infinity. The archimedean assumption is convenient to get a statement that works on ℕ, ℤ and ℝ, although not necessary (a version in ordered fields is given in Filter.Tendsto.atTop_mul_const).

source
theorem Filter.Tendsto.atTop_mul_const_of_neg' {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [LinearOrderedRing R] [Archimedean R] (hr : r < 0) (hf : Filter.Tendsto f l Filter.atTop) :
Filter.Tendsto (fun (x : α) => f x * r) l Filter.atBot

See also Filter.Tendsto.atTop_mul_const_of_neg for a version of this lemma for LinearOrderedFields which does not require the Archimedean assumption.

source
theorem Filter.Tendsto.atBot_mul_const' {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [LinearOrderedRing R] [Archimedean R] (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atBot) :
Filter.Tendsto (fun (x : α) => f x * r) l Filter.atBot

See also Filter.Tendsto.atBot_mul_const for a version of this lemma for LinearOrderedFields which does not require the Archimedean assumption.

source
theorem Filter.Tendsto.atBot_mul_const_of_neg' {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [LinearOrderedRing R] [Archimedean R] (hr : r < 0) (hf : Filter.Tendsto f l Filter.atBot) :
Filter.Tendsto (fun (x : α) => f x * r) l Filter.atTop

See also Filter.Tendsto.atBot_mul_const_of_neg for a version of this lemma for LinearOrderedFields which does not require the Archimedean assumption.

source
@[deprecated Filter.Tendsto.atTop_mul_const_of_neg']
theorem Filter.Tendsto.atTop_mul_neg_const' {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [LinearOrderedRing R] [Archimedean R] (hr : r < 0) (hf : Filter.Tendsto f l Filter.atTop) :
Filter.Tendsto (fun (x : α) => f x * r) l Filter.atBot

Alias of Filter.Tendsto.atTop_mul_const_of_neg'.

See also Filter.Tendsto.atTop_mul_const_of_neg for a version of this lemma for LinearOrderedFields which does not require the Archimedean assumption.

source
@[deprecated Filter.Tendsto.atBot_mul_const_of_neg']
theorem Filter.Tendsto.atBot_mul_neg_const' {α : Type u_1} {R : Type u_2} {l : Filter α} {f : α → R} {r : R} [LinearOrderedRing R] [Archimedean R] (hr : r < 0) (hf : Filter.Tendsto f l Filter.atBot) :
Filter.Tendsto (fun (x : α) => f x * r) l Filter.atTop

Alias of Filter.Tendsto.atBot_mul_const_of_neg'.

See also Filter.Tendsto.atBot_mul_const_of_neg for a version of this lemma for LinearOrderedFields which does not require the Archimedean assumption.

source
theorem Filter.Tendsto.atTop_nsmul_const {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [LinearOrderedCancelAddCommMonoid R] [Archimedean R] {f : α → ℕ} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atTop) :
Filter.Tendsto (fun (x : α) => f x • r) l Filter.atTop
source
theorem Filter.Tendsto.atTop_nsmul_neg_const {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [LinearOrderedAddCommGroup R] [Archimedean R] {f : α → ℕ} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atTop) :
Filter.Tendsto (fun (x : α) => f x • r) l Filter.atBot
source
theorem Filter.Tendsto.atTop_zsmul_const {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [LinearOrderedAddCommGroup R] [Archimedean R] {f : α → ℤ} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atTop) :
Filter.Tendsto (fun (x : α) => f x • r) l Filter.atTop
source
theorem Filter.Tendsto.atTop_zsmul_neg_const {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [LinearOrderedAddCommGroup R] [Archimedean R] {f : α → ℤ} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atTop) :
Filter.Tendsto (fun (x : α) => f x • r) l Filter.atBot
source
theorem Filter.Tendsto.atBot_zsmul_const {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [LinearOrderedAddCommGroup R] [Archimedean R] {f : α → ℤ} (hr : 0 < r) (hf : Filter.Tendsto f l Filter.atBot) :
Filter.Tendsto (fun (x : α) => f x • r) l Filter.atBot
source
theorem Filter.Tendsto.atBot_zsmul_neg_const {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [LinearOrderedAddCommGroup R] [Archimedean R] {f : α → ℤ} (hr : r < 0) (hf : Filter.Tendsto f l Filter.atBot) :
Filter.Tendsto (fun (x : α) => f x • r) l Filter.atTop