Filter.atTop and Filter.atBot filters on preorders, monoids and groups. #
In this file we define the filters
Filter.atTop: corresponds ton → +∞;Filter.atBot: corresponds ton → -∞.
Then we prove many lemmas like “if f → +∞, then f ± c → +∞”.
atTop is the filter representing the limit → ∞ on an ordered set.
It is generated by the collection of up-sets {b | a ≤ b}.
(The preorder need not have a top element for this to be well defined,
and indeed is trivial when a top element exists.)
Equations
- Filter.atTop = ⨅ (a : α), Filter.principal (Set.Ici a)
Instances For
atBot is the filter representing the limit → -∞ on an ordered set.
It is generated by the collection of down-sets {b | b ≤ a}.
(The preorder need not have a bottom element for this to be well defined,
and indeed is trivial when a bottom element exists.)
Equations
- Filter.atBot = ⨅ (a : α), Filter.principal (Set.Iic a)
Instances For
theorem
Filter.disjoint_pure_atTop
{α : Type u_3}
[Preorder α]
[NoMaxOrder α]
(x : α)
:
Disjoint (pure x) Filter.atTop
theorem
Filter.disjoint_pure_atBot
{α : Type u_3}
[Preorder α]
[NoMinOrder α]
(x : α)
:
Disjoint (pure x) Filter.atBot
theorem
Filter.not_tendsto_const_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[NoMaxOrder α]
(x : α)
(l : Filter β)
[l.NeBot]
:
¬Filter.Tendsto (fun (x_1 : β) => x) l Filter.atTop
theorem
Filter.not_tendsto_const_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[NoMinOrder α]
(x : α)
(l : Filter β)
[l.NeBot]
:
¬Filter.Tendsto (fun (x_1 : β) => x) l Filter.atBot
theorem
Filter.eventually_ge_atTop
{α : Type u_3}
[Preorder α]
(a : α)
:
∀ᶠ (x : α) in Filter.atTop, a ≤ x
theorem
Filter.eventually_le_atBot
{α : Type u_3}
[Preorder α]
(a : α)
:
∀ᶠ (x : α) in Filter.atBot, x ≤ a
theorem
Filter.eventually_gt_atTop
{α : Type u_3}
[Preorder α]
[NoMaxOrder α]
(a : α)
:
∀ᶠ (x : α) in Filter.atTop, a < x
theorem
Filter.eventually_ne_atTop
{α : Type u_3}
[Preorder α]
[NoMaxOrder α]
(a : α)
:
∀ᶠ (x : α) in Filter.atTop, x ≠ a
theorem
Filter.Tendsto.eventually_gt_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder β]
[NoMaxOrder β]
{f : α → β}
{l : Filter α}
(hf : Filter.Tendsto f l Filter.atTop)
(c : β)
:
∀ᶠ (x : α) in l, c < f x
theorem
Filter.Tendsto.eventually_ge_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder β]
{f : α → β}
{l : Filter α}
(hf : Filter.Tendsto f l Filter.atTop)
(c : β)
:
∀ᶠ (x : α) in l, c ≤ f x
theorem
Filter.Tendsto.eventually_ne_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder β]
[NoMaxOrder β]
{f : α → β}
{l : Filter α}
(hf : Filter.Tendsto f l Filter.atTop)
(c : β)
:
∀ᶠ (x : α) in l, f x ≠ c
theorem
Filter.Tendsto.eventually_ne_atTop'
{α : Type u_3}
{β : Type u_4}
[Preorder β]
[NoMaxOrder β]
{f : α → β}
{l : Filter α}
(hf : Filter.Tendsto f l Filter.atTop)
(c : α)
:
∀ᶠ (x : α) in l, x ≠ c
theorem
Filter.eventually_lt_atBot
{α : Type u_3}
[Preorder α]
[NoMinOrder α]
(a : α)
:
∀ᶠ (x : α) in Filter.atBot, x < a
theorem
Filter.eventually_ne_atBot
{α : Type u_3}
[Preorder α]
[NoMinOrder α]
(a : α)
:
∀ᶠ (x : α) in Filter.atBot, x ≠ a
theorem
Filter.Tendsto.eventually_lt_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder β]
[NoMinOrder β]
{f : α → β}
{l : Filter α}
(hf : Filter.Tendsto f l Filter.atBot)
(c : β)
:
∀ᶠ (x : α) in l, f x < c
theorem
Filter.Tendsto.eventually_le_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder β]
{f : α → β}
{l : Filter α}
(hf : Filter.Tendsto f l Filter.atBot)
(c : β)
:
∀ᶠ (x : α) in l, f x ≤ c
theorem
Filter.Tendsto.eventually_ne_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder β]
[NoMinOrder β]
{f : α → β}
{l : Filter α}
(hf : Filter.Tendsto f l Filter.atBot)
(c : β)
:
∀ᶠ (x : α) in l, f x ≠ c
theorem
Filter.eventually_forall_ge_atTop
{α : Type u_3}
[Preorder α]
{p : α → Prop}
:
(∀ᶠ (x : α) in Filter.atTop, ∀ (y : α), x ≤ y → p y) ↔ ∀ᶠ (x : α) in Filter.atTop, p x
theorem
Filter.eventually_forall_le_atBot
{α : Type u_3}
[Preorder α]
{p : α → Prop}
:
(∀ᶠ (x : α) in Filter.atBot, ∀ y ≤ x, p y) ↔ ∀ᶠ (x : α) in Filter.atBot, p x
theorem
Filter.Tendsto.eventually_forall_ge_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder β]
{l : Filter α}
{p : β → Prop}
{f : α → β}
(hf : Filter.Tendsto f l Filter.atTop)
(h_evtl : ∀ᶠ (x : β) in Filter.atTop, p x)
:
∀ᶠ (x : α) in l, ∀ (y : β), f x ≤ y → p y
theorem
Filter.Tendsto.eventually_forall_le_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder β]
{l : Filter α}
{p : β → Prop}
{f : α → β}
(hf : Filter.Tendsto f l Filter.atBot)
(h_evtl : ∀ᶠ (x : β) in Filter.atBot, p x)
:
∀ᶠ (x : α) in l, ∀ y ≤ f x, p y
theorem
Filter.tendsto_atTop_pure
{α : Type u_3}
{β : Type u_4}
[PartialOrder α]
[OrderTop α]
(f : α → β)
:
Filter.Tendsto f Filter.atTop (pure (f ⊤))
theorem
Filter.tendsto_atBot_pure
{α : Type u_3}
{β : Type u_4}
[PartialOrder α]
[OrderBot α]
(f : α → β)
:
Filter.Tendsto f Filter.atBot (pure (f ⊥))
theorem
Filter.Frequently.forall_exists_of_atTop
{α : Type u_3}
[Preorder α]
{p : α → Prop}
(h : ∃ᶠ (x : α) in Filter.atTop, p x)
(a : α)
:
∃ b ≥ a, p b
theorem
Filter.Frequently.forall_exists_of_atBot
{α : Type u_3}
[Preorder α]
{p : α → Prop}
(h : ∃ᶠ (x : α) in Filter.atBot, p x)
(a : α)
:
∃ b ≤ a, p b
theorem
Filter.hasAntitoneBasis_atTop
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[Nonempty α]
:
Filter.atTop.HasAntitoneBasis Set.Ici
theorem
Filter.atTop_basis
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[Nonempty α]
:
Filter.atTop.HasBasis (fun (x : α) => True) Set.Ici
theorem
Filter.atTop_basis_Ioi
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[Nonempty α]
[NoMaxOrder α]
:
Filter.atTop.HasBasis (fun (x : α) => True) Set.Ioi
theorem
Filter.atTop_basis_Ioi'
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[NoMaxOrder α]
(a : α)
:
Filter.atTop.HasBasis (fun (x : α) => a < x) Set.Ioi
theorem
Filter.atTop_basis'
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
Filter.atTop.HasBasis (fun (x : α) => a ≤ x) Set.Ici
instance
Filter.atTop_neBot
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[Nonempty α]
:
Filter.atTop.NeBot
theorem
Filter.atTop_neBot_iff
{α : Type u_6}
[Preorder α]
:
Filter.atTop.NeBot ↔ Nonempty α ∧ IsDirected α fun (x1 x2 : α) => x1 ≤ x2
theorem
Filter.atBot_neBot_iff
{α : Type u_6}
[Preorder α]
:
Filter.atBot.NeBot ↔ Nonempty α ∧ IsDirected α fun (x1 x2 : α) => x1 ≥ x2
@[simp]
theorem
Filter.mem_atTop_sets
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[Nonempty α]
{s : Set α}
:
s ∈ Filter.atTop ↔ ∃ (a : α), ∀ b ≥ a, b ∈ s
@[simp]
theorem
Filter.eventually_atTop
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{p : α → Prop}
[Nonempty α]
:
(∀ᶠ (x : α) in Filter.atTop, p x) ↔ ∃ (a : α), ∀ b ≥ a, p b
theorem
Filter.frequently_atTop
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{p : α → Prop}
[Nonempty α]
:
(∃ᶠ (x : α) in Filter.atTop, p x) ↔ ∀ (a : α), ∃ b ≥ a, p b
theorem
Filter.Eventually.exists_forall_of_atTop
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{p : α → Prop}
[Nonempty α]
:
(∀ᶠ (x : α) in Filter.atTop, p x) → ∃ (a : α), ∀ b ≥ a, p b
Alias of the forward direction of Filter.eventually_atTop.
theorem
Filter.exists_eventually_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[Nonempty α]
{r : α → β → Prop}
:
(∃ (b : β), ∀ᶠ (a : α) in Filter.atTop, r a b) ↔ ∀ᶠ (a₀ : α) in Filter.atTop, ∃ (b : β), ∀ a ≥ a₀, r a b
theorem
Filter.map_atTop_eq
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[Nonempty α]
{f : α → β}
:
Filter.map f Filter.atTop = ⨅ (a : α), Filter.principal (f '' {a' : α | a ≤ a'})
theorem
Filter.frequently_atTop'
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{p : α → Prop}
[Nonempty α]
[NoMaxOrder α]
:
(∃ᶠ (x : α) in Filter.atTop, p x) ↔ ∀ (a : α), ∃ b > a, p b
theorem
Filter.atBot_basis_Iio
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[Nonempty α]
[NoMinOrder α]
:
Filter.atBot.HasBasis (fun (x : α) => True) Set.Iio
theorem
Filter.atBot_basis_Iio'
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[NoMinOrder α]
(a : α)
:
Filter.atBot.HasBasis (fun (x : α) => x < a) Set.Iio
theorem
Filter.atBot_basis'
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
(a : α)
:
Filter.atBot.HasBasis (fun (x : α) => x ≤ a) Set.Iic
theorem
Filter.atBot_basis
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[Nonempty α]
:
Filter.atBot.HasBasis (fun (x : α) => True) Set.Iic
instance
Filter.atBot_neBot
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[Nonempty α]
:
Filter.atBot.NeBot
@[simp]
theorem
Filter.mem_atBot_sets
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[Nonempty α]
{s : Set α}
:
s ∈ Filter.atBot ↔ ∃ (a : α), ∀ b ≤ a, b ∈ s
@[simp]
theorem
Filter.eventually_atBot
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{p : α → Prop}
[Nonempty α]
:
(∀ᶠ (x : α) in Filter.atBot, p x) ↔ ∃ (a : α), ∀ b ≤ a, p b
theorem
Filter.frequently_atBot
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{p : α → Prop}
[Nonempty α]
:
(∃ᶠ (x : α) in Filter.atBot, p x) ↔ ∀ (a : α), ∃ b ≤ a, p b
theorem
Filter.Eventually.exists_forall_of_atBot
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{p : α → Prop}
[Nonempty α]
:
(∀ᶠ (x : α) in Filter.atBot, p x) → ∃ (a : α), ∀ b ≤ a, p b
Alias of the forward direction of Filter.eventually_atBot.
theorem
Filter.exists_eventually_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[Nonempty α]
{r : α → β → Prop}
:
(∃ (b : β), ∀ᶠ (a : α) in Filter.atBot, r a b) ↔ ∀ᶠ (a₀ : α) in Filter.atBot, ∃ (b : β), ∀ a ≤ a₀, r a b
theorem
Filter.map_atBot_eq
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[Nonempty α]
{f : α → β}
:
Filter.map f Filter.atBot = ⨅ (a : α), Filter.principal (f '' {a' : α | a' ≤ a})
theorem
Filter.frequently_atBot'
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{p : α → Prop}
[Nonempty α]
[NoMinOrder α]
:
(∃ᶠ (x : α) in Filter.atBot, p x) ↔ ∀ (a : α), ∃ b < a, p b
theorem
Filter.tendsto_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder β]
{m : α → β}
{f : Filter α}
:
Filter.Tendsto m f Filter.atTop ↔ ∀ (b : β), ∀ᶠ (a : α) in f, b ≤ m a
theorem
Filter.tendsto_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder β]
{m : α → β}
{f : Filter α}
:
Filter.Tendsto m f Filter.atBot ↔ ∀ (b : β), ∀ᶠ (a : α) in f, m a ≤ b
theorem
Filter.tendsto_atTop_mono'
{α : Type u_3}
{β : Type u_4}
[Preorder β]
(l : Filter α)
⦃f₁ f₂ : α → β⦄
(h : f₁ ≤ᶠ[l] f₂)
(h₁ : Filter.Tendsto f₁ l Filter.atTop)
:
theorem
Filter.tendsto_atBot_mono'
{α : Type u_3}
{β : Type u_4}
[Preorder β]
(l : Filter α)
⦃f₁ f₂ : α → β⦄
(h : f₁ ≤ᶠ[l] f₂)
:
Filter.Tendsto f₂ l Filter.atBot → Filter.Tendsto f₁ l Filter.atBot
theorem
Filter.tendsto_atTop_mono
{α : Type u_3}
{β : Type u_4}
[Preorder β]
{l : Filter α}
{f g : α → β}
(h : ∀ (n : α), f n ≤ g n)
:
Filter.Tendsto f l Filter.atTop → Filter.Tendsto g l Filter.atTop
theorem
Filter.tendsto_atBot_mono
{α : Type u_3}
{β : Type u_4}
[Preorder β]
{l : Filter α}
{f g : α → β}
(h : ∀ (n : α), f n ≤ g n)
:
Filter.Tendsto g l Filter.atBot → Filter.Tendsto f l Filter.atBot
theorem
Filter.atTop_eq_generate_of_forall_exists_le
{α : Type u_3}
[LinearOrder α]
{s : Set α}
(hs : ∀ (x : α), ∃ y ∈ s, x ≤ y)
:
theorem
Filter.atTop_eq_generate_of_not_bddAbove
{α : Type u_3}
[LinearOrder α]
{s : Set α}
(hs : ¬BddAbove s)
:
@[simp]
theorem
OrderIso.tendsto_atTop_iff
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder α]
[Preorder β]
{l : Filter γ}
{f : γ → α}
(e : α ≃o β)
:
Filter.Tendsto (fun (x : γ) => e (f x)) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
@[simp]
theorem
OrderIso.tendsto_atBot_iff
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder α]
[Preorder β]
{l : Filter γ}
{f : γ → α}
(e : α ≃o β)
:
Filter.Tendsto (fun (x : γ) => e (f x)) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
Sequences #
theorem
Filter.extraction_of_frequently_atTop'
{P : ℕ → Prop}
(h : ∀ (N : ℕ), ∃ n > N, P n)
:
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
theorem
Filter.extraction_of_frequently_atTop
{P : ℕ → Prop}
(h : ∃ᶠ (n : ℕ) in Filter.atTop, P n)
:
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
theorem
Filter.extraction_of_eventually_atTop
{P : ℕ → Prop}
(h : ∀ᶠ (n : ℕ) in Filter.atTop, P n)
:
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P (φ n)
theorem
Filter.extraction_forall_of_frequently
{P : ℕ → ℕ → Prop}
(h : ∀ (n : ℕ), ∃ᶠ (k : ℕ) in Filter.atTop, P n k)
:
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
theorem
Filter.extraction_forall_of_eventually
{P : ℕ → ℕ → Prop}
(h : ∀ (n : ℕ), ∀ᶠ (k : ℕ) in Filter.atTop, P n k)
:
∃ (φ : ℕ → ℕ), StrictMono φ ∧ ∀ (n : ℕ), P n (φ n)
theorem
Filter.Eventually.atTop_of_arithmetic
{p : ℕ → Prop}
{n : ℕ}
(hn : n ≠ 0)
(hp : ∀ k < n, ∀ᶠ (a : ℕ) in Filter.atTop, p (n * a + k))
:
∀ᶠ (a : ℕ) in Filter.atTop, p a
theorem
Filter.inf_map_atTop_neBot_iff
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{F : Filter β}
{u : α → β}
[Nonempty α]
:
(F ⊓ Filter.map u Filter.atTop).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≥ N, u n ∈ U
theorem
Filter.exists_le_of_tendsto_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{u : α → β}
[Preorder β]
(h : Filter.Tendsto u Filter.atTop Filter.atTop)
(a : α)
(b : β)
:
∃ a' ≥ a, b ≤ u a'
theorem
Filter.exists_le_of_tendsto_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{u : α → β}
[Preorder β]
(h : Filter.Tendsto u Filter.atTop Filter.atBot)
(a : α)
(b : β)
:
∃ a' ≥ a, u a' ≤ b
theorem
Filter.exists_lt_of_tendsto_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{u : α → β}
[Preorder β]
[NoMaxOrder β]
(h : Filter.Tendsto u Filter.atTop Filter.atTop)
(a : α)
(b : β)
:
∃ a' ≥ a, b < u a'
theorem
Filter.exists_lt_of_tendsto_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{u : α → β}
[Preorder β]
[NoMinOrder β]
(h : Filter.Tendsto u Filter.atTop Filter.atBot)
(a : α)
(b : β)
:
∃ a' ≥ a, u a' < b
theorem
Filter.inf_map_atBot_neBot_iff
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{F : Filter β}
{u : α → β}
:
(F ⊓ Filter.map u Filter.atBot).NeBot ↔ ∀ U ∈ F, ∀ (N : α), ∃ n ≤ N, u n ∈ U
theorem
Filter.high_scores
{β : Type u_4}
[LinearOrder β]
[NoMaxOrder β]
{u : ℕ → β}
(hu : Filter.Tendsto u Filter.atTop Filter.atTop)
(N : ℕ)
:
∃ n ≥ N, ∀ k < n, u k < u n
If u is a sequence which is unbounded above,
then after any point, it reaches a value strictly greater than all previous values.
theorem
Filter.low_scores
{β : Type u_4}
[LinearOrder β]
[NoMinOrder β]
{u : ℕ → β}
(hu : Filter.Tendsto u Filter.atTop Filter.atBot)
(N : ℕ)
:
∃ n ≥ N, ∀ k < n, u n < u k
If u is a sequence which is unbounded below,
then after any point, it reaches a value strictly smaller than all previous values.
theorem
Filter.frequently_high_scores
{β : Type u_4}
[LinearOrder β]
[NoMaxOrder β]
{u : ℕ → β}
(hu : Filter.Tendsto u Filter.atTop Filter.atTop)
:
∃ᶠ (n : ℕ) in Filter.atTop, ∀ k < n, u k < u n
If u is a sequence which is unbounded above,
then it Frequently reaches a value strictly greater than all previous values.
theorem
Filter.frequently_low_scores
{β : Type u_4}
[LinearOrder β]
[NoMinOrder β]
{u : ℕ → β}
(hu : Filter.Tendsto u Filter.atTop Filter.atBot)
:
∃ᶠ (n : ℕ) in Filter.atTop, ∀ k < n, u n < u k
If u is a sequence which is unbounded below,
then it Frequently reaches a value strictly smaller than all previous values.
theorem
Filter.strictMono_subseq_of_tendsto_atTop
{β : Type u_4}
[LinearOrder β]
[NoMaxOrder β]
{u : ℕ → β}
(hu : Filter.Tendsto u Filter.atTop Filter.atTop)
:
∃ (φ : ℕ → ℕ), StrictMono φ ∧ StrictMono (u ∘ φ)
theorem
Filter.strictMono_subseq_of_id_le
{u : ℕ → ℕ}
(hu : ∀ (n : ℕ), n ≤ u n)
:
∃ (φ : ℕ → ℕ), StrictMono φ ∧ StrictMono (u ∘ φ)
theorem
Monotone.upperBounds_range_comp_tendsto_atTop
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[Preorder γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Monotone f)
{g : α → β}
(hg : Filter.Tendsto g l Filter.atTop)
:
upperBounds (Set.range (f ∘ g)) = upperBounds (Set.range f)
If f is a monotone function and g tends to atTop along a nontrivial filter.
then the upper bounds of the range of f ∘ g
are the same as the upper bounds of the range of f.
This lemma together with exists_seq_monotone_tendsto_atTop_atTop below
is useful to reduce a statement
about a monotone family indexed by a type with countably generated atTop (e.g., ℝ)
to the case of a family indexed by natural numbers.
theorem
Monotone.lowerBounds_range_comp_tendsto_atBot
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[Preorder γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Monotone f)
{g : α → β}
(hg : Filter.Tendsto g l Filter.atBot)
:
lowerBounds (Set.range (f ∘ g)) = lowerBounds (Set.range f)
If f is a monotone function and g tends to atBot along a nontrivial filter.
then the lower bounds of the range of f ∘ g
are the same as the lower bounds of the range of f.
theorem
Antitone.lowerBounds_range_comp_tendsto_atTop
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[Preorder γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Antitone f)
{g : α → β}
(hg : Filter.Tendsto g l Filter.atTop)
:
lowerBounds (Set.range (f ∘ g)) = lowerBounds (Set.range f)
If f is an antitone function and g tends to atTop along a nontrivial filter.
then the upper bounds of the range of f ∘ g
are the same as the upper bounds of the range of f.
theorem
Antitone.upperBounds_range_comp_tendsto_atBot
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[Preorder γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Antitone f)
{g : α → β}
(hg : Filter.Tendsto g l Filter.atBot)
:
upperBounds (Set.range (f ∘ g)) = upperBounds (Set.range f)
If f is an antitone function and g tends to atBot along a nontrivial filter.
then the upper bounds of the range of f ∘ g
are the same as the upper bounds of the range of f.
theorem
Monotone.ciSup_comp_tendsto_atTop
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[ConditionallyCompleteLattice γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Monotone f)
(hb : BddAbove (Set.range f))
{g : α → β}
(hg : Filter.Tendsto g l Filter.atTop)
:
⨆ (a : α), f (g a) = ⨆ (b : β), f b
If f is a monotone function with bounded range
and g tends to atTop along a nontrivial filter,
then the indexed supremum of f ∘ g is equal to the indexed supremum of f.
The assumption BddAbove (range f) can be omitted,
if the codomain of f is a conditionally complete linear order or a complete lattice, see below.
theorem
Monotone.ciInf_comp_tendsto_atBot
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[ConditionallyCompleteLattice γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Monotone f)
(hb : BddBelow (Set.range f))
{g : α → β}
(hg : Filter.Tendsto g l Filter.atBot)
:
⨅ (a : α), f (g a) = ⨅ (b : β), f b
If f is a monotone function with bounded range
and g tends to atBot along a nontrivial filter,
then the indexed infimum of f ∘ g is equal to the indexed infimum of f.
The assumption BddBelow (range f) can be omitted,
if the codomain of f is a conditionally complete linear order or a complete lattice, see below.
theorem
Antitone.ciSup_comp_tendsto_atBot
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[ConditionallyCompleteLattice γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Antitone f)
(hb : BddAbove (Set.range f))
{g : α → β}
(hg : Filter.Tendsto g l Filter.atBot)
:
⨆ (a : α), f (g a) = ⨆ (b : β), f b
If f is an antitone function with bounded range
and g tends to atBot along a nontrivial filter,
then the indexed supremum of f ∘ g is equal to the indexed supremum of f.
The assumption BddAbove (range f) can be omitted,
if the codomain of f is a conditionally complete linear order or a complete lattice, see below.
theorem
Antitone.ciInf_comp_tendsto_atTop
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[ConditionallyCompleteLattice γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Antitone f)
(hb : BddBelow (Set.range f))
{g : α → β}
(hg : Filter.Tendsto g l Filter.atTop)
:
⨅ (a : α), f (g a) = ⨅ (b : β), f b
If f is an antitone function with bounded range
and g tends to atTop along a nontrivial filter,
then the indexed infimum of f ∘ g is equal to the indexed infimum of f.
The assumption BddBelow (range f) can be omitted,
if the codomain of f is a conditionally complete linear order or a complete lattice, see below.
theorem
Monotone.ciSup_comp_tendsto_atTop_of_linearOrder
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[ConditionallyCompleteLinearOrder γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Monotone f)
{g : α → β}
(hg : Filter.Tendsto g l Filter.atTop)
:
⨆ (a : α), f (g a) = ⨆ (b : β), f b
If f is a monotone function taking values in a conditionally complete linear order
and g tends to atTop along a nontrivial filter,
then the indexed supremum of f ∘ g is equal to the indexed supremum of f.
theorem
Monotone.ciInf_comp_tendsto_atBot_of_linearOrder
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[ConditionallyCompleteLinearOrder γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Monotone f)
{g : α → β}
(hg : Filter.Tendsto g l Filter.atBot)
:
⨅ (a : α), f (g a) = ⨅ (b : β), f b
If f is a monotone function taking values in a conditionally complete linear order
and g tends to atBot along a nontrivial filter,
then the indexed infimum of f ∘ g is equal to the indexed infimum of f.
theorem
Antitone.ciInf_comp_tendsto_atTop_of_linearOrder
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[ConditionallyCompleteLinearOrder γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Antitone f)
{g : α → β}
(hg : Filter.Tendsto g l Filter.atTop)
:
⨅ (a : α), f (g a) = ⨅ (b : β), f b
If f is an antitone function taking values in a conditionally complete linear order
and g tends to atTop along a nontrivial filter,
then the indexed infimum of f ∘ g is equal to the indexed infimum of f.
theorem
Antitone.ciSup_comp_tendsto_atBot_of_linearOrder
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[ConditionallyCompleteLinearOrder γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Antitone f)
{g : α → β}
(hg : Filter.Tendsto g l Filter.atBot)
:
⨆ (a : α), f (g a) = ⨆ (b : β), f b
If f is an antitone function taking values in a conditionally complete linear order
and g tends to atBot along a nontrivial filter,
then the indexed supremum of f ∘ g is equal to the indexed supremum of f.
theorem
Monotone.iSup_comp_tendsto_atTop
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[ConditionallyCompleteLattice γ]
[OrderTop γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Monotone f)
{g : α → β}
(hg : Filter.Tendsto g l Filter.atTop)
:
⨆ (a : α), f (g a) = ⨆ (b : β), f b
If f is a monotone function taking values in a complete lattice
and g tends to atTop along a nontrivial filter,
then the indexed supremum of f ∘ g is equal to the indexed supremum of f.
theorem
Monotone.iInf_comp_tendsto_atBot
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[ConditionallyCompleteLattice γ]
[OrderBot γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Monotone f)
{g : α → β}
(hg : Filter.Tendsto g l Filter.atBot)
:
⨅ (a : α), f (g a) = ⨅ (b : β), f b
If f is a monotone function taking values in a complete lattice
and g tends to atBot along a nontrivial filter,
then the indexed infimum of f ∘ g is equal to the indexed infimum of f.
theorem
Antitone.iSup_comp_tendsto_atBot
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[ConditionallyCompleteLattice γ]
[OrderTop γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Antitone f)
{g : α → β}
(hg : Filter.Tendsto g l Filter.atBot)
:
⨆ (a : α), f (g a) = ⨆ (b : β), f b
If f is an antitone function taking values in a complete lattice
and g tends to atBot along a nontrivial filter,
then the indexed supremum of f ∘ g is equal to the indexed supremum of f.
theorem
Antitone.iInf_comp_tendsto_atTop
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[ConditionallyCompleteLattice γ]
[OrderBot γ]
{l : Filter α}
[l.NeBot]
{f : β → γ}
(hf : Antitone f)
{g : α → β}
(hg : Filter.Tendsto g l Filter.atTop)
:
⨅ (a : α), f (g a) = ⨅ (b : β), f b
If f is an antitone function taking values in a complete lattice
and g tends to atTop along a nontrivial filter,
then the indexed infimum of f ∘ g is equal to the indexed infimum of f.
theorem
Monotone.iUnion_comp_tendsto_atTop
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
{l : Filter α}
[l.NeBot]
{s : β → Set γ}
(hs : Monotone s)
{f : α → β}
(hf : Filter.Tendsto f l Filter.atTop)
:
⋃ (a : α), s (f a) = ⋃ (b : β), s b
If s is a monotone family of sets and f tends to atTop along a nontrivial filter,
then the indexed union of s ∘ f is equal to the indexed union of s.
theorem
Monotone.iInter_comp_tendsto_atBot
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
{l : Filter α}
[l.NeBot]
{s : β → Set γ}
(hs : Monotone s)
{f : α → β}
(hf : Filter.Tendsto f l Filter.atBot)
:
⋂ (a : α), s (f a) = ⋂ (b : β), s b
If s is a monotone family of sets and f tends to atBot along a nontrivial filter,
then the indexed intersection of s ∘ f is equal to the indexed intersection of s.
theorem
Antitone.iInter_comp_tendsto_atTop
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
{l : Filter α}
[l.NeBot]
{s : β → Set γ}
(hs : Antitone s)
{f : α → β}
(hf : Filter.Tendsto f l Filter.atTop)
:
⋂ (a : α), s (f a) = ⋂ (b : β), s b
If s is an antitone family of sets and f tends to atTop along a nontrivial filter,
then the indexed intersection of s ∘ f is equal to the indexed intersection of s.
theorem
Antitone.iUnion_comp_tendsto_atBot
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
{l : Filter α}
[l.NeBot]
{s : β → Set γ}
(hs : Antitone s)
{f : α → β}
(hf : Filter.Tendsto f l Filter.atBot)
:
⋃ (a : α), s (f a) = ⋃ (b : β), s b
If s is a monotone family of sets and f tends to atBot along a nontrivial filter,
then the indexed union of s ∘ f is equal to the indexed union of s.
theorem
Filter.tendsto_atTop'
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{f : α → β}
{l : Filter β}
:
Filter.Tendsto f Filter.atTop l ↔ ∀ s ∈ l, ∃ (a : α), ∀ b ≥ a, f b ∈ s
theorem
Filter.tendsto_atTop_principal
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{f : α → β}
{s : Set β}
:
Filter.Tendsto f Filter.atTop (Filter.principal s) ↔ ∃ (N : α), ∀ n ≥ N, f n ∈ s
theorem
Filter.tendsto_atTop_atTop
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{f : α → β}
[Preorder β]
:
Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), i ≤ a → b ≤ f a
A function f grows to +∞ independent of an order-preserving embedding e.
theorem
Filter.tendsto_atTop_atBot
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{f : α → β}
[Preorder β]
:
Filter.Tendsto f Filter.atTop Filter.atBot ↔ ∀ (b : β), ∃ (i : α), ∀ (a : α), i ≤ a → f a ≤ b
theorem
Filter.tendsto_atTop_atTop_iff_of_monotone
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{f : α → β}
[Preorder β]
(hf : Monotone f)
:
Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ (a : α), b ≤ f a
theorem
Filter.tendsto_atTop_atBot_iff_of_antitone
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{f : α → β}
[Preorder β]
(hf : Antitone f)
:
Filter.Tendsto f Filter.atTop Filter.atBot ↔ ∀ (b : β), ∃ (a : α), f a ≤ b
theorem
Filter.tendsto_atBot'
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{f : α → β}
{l : Filter β}
:
Filter.Tendsto f Filter.atBot l ↔ ∀ s ∈ l, ∃ (a : α), ∀ b ≤ a, f b ∈ s
theorem
Filter.tendsto_atBot_principal
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{f : α → β}
{s : Set β}
:
Filter.Tendsto f Filter.atBot (Filter.principal s) ↔ ∃ (N : α), ∀ n ≤ N, f n ∈ s
theorem
Filter.tendsto_atBot_atTop
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{f : α → β}
[Preorder β]
:
Filter.Tendsto f Filter.atBot Filter.atTop ↔ ∀ (b : β), ∃ (i : α), ∀ a ≤ i, b ≤ f a
theorem
Filter.tendsto_atBot_atBot
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{f : α → β}
[Preorder β]
:
Filter.Tendsto f Filter.atBot Filter.atBot ↔ ∀ (b : β), ∃ (i : α), ∀ a ≤ i, f a ≤ b
theorem
Filter.tendsto_atBot_atBot_iff_of_monotone
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{f : α → β}
[Preorder β]
(hf : Monotone f)
:
Filter.Tendsto f Filter.atBot Filter.atBot ↔ ∀ (b : β), ∃ (a : α), f a ≤ b
theorem
Filter.tendsto_atBot_atTop_iff_of_antitone
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{f : α → β}
[Preorder β]
(hf : Antitone f)
:
Filter.Tendsto f Filter.atBot Filter.atTop ↔ ∀ (b : β), ∃ (a : α), b ≤ f a
theorem
Monotone.tendsto_atTop_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[Preorder β]
{f : α → β}
(hf : Monotone f)
(h : ∀ (b : β), ∃ (a : α), b ≤ f a)
:
Alias of Filter.tendsto_atTop_atTop_of_monotone.
theorem
Monotone.tendsto_atBot_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[Preorder β]
{f : α → β}
(hf : Monotone f)
(h : ∀ (b : β), ∃ (a : α), f a ≤ b)
:
Alias of Filter.tendsto_atBot_atBot_of_monotone.
theorem
Monotone.tendsto_atTop_atTop_iff
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{f : α → β}
[Preorder β]
(hf : Monotone f)
:
Filter.Tendsto f Filter.atTop Filter.atTop ↔ ∀ (b : β), ∃ (a : α), b ≤ f a
theorem
Monotone.tendsto_atBot_atBot_iff
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{f : α → β}
[Preorder β]
(hf : Monotone f)
:
Filter.Tendsto f Filter.atBot Filter.atBot ↔ ∀ (b : β), ∃ (a : α), f a ≤ b
theorem
Filter.tendsto_atTop_embedding
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[Preorder γ]
{f : α → β}
{e : β → γ}
{l : Filter α}
(hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂)
(hu : ∀ (c : γ), ∃ (b : β), c ≤ e b)
:
Filter.Tendsto (e ∘ f) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
theorem
Filter.tendsto_atBot_embedding
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder β]
[Preorder γ]
{f : α → β}
{e : β → γ}
{l : Filter α}
(hm : ∀ (b₁ b₂ : β), e b₁ ≤ e b₂ ↔ b₁ ≤ b₂)
(hu : ∀ (c : γ), ∃ (b : β), e b ≤ c)
:
Filter.Tendsto (e ∘ f) l Filter.atBot ↔ Filter.Tendsto f l Filter.atBot
A function f goes to -∞ independent of an order-preserving embedding e.
theorem
Filter.atTop_finset_eq_iInf
{α : Type u_3}
:
Filter.atTop = ⨅ (x : α), Filter.principal (Set.Ici {x})
theorem
Monotone.tendsto_atTop_finset
{α : Type u_3}
{β : Type u_4}
[Preorder β]
{f : β → Finset α}
(h : Monotone f)
(h' : ∀ (x : α), ∃ (n : β), x ∈ f n)
:
Alias of Filter.tendsto_atTop_finset_of_monotone.
If f is a monotone sequence of Finsets and each x belongs to one of f n, then
Tendsto f atTop atTop.
theorem
Filter.tendsto_finset_image_atTop_atTop
{β : Type u_4}
{γ : Type u_5}
[DecidableEq β]
{i : β → γ}
{j : γ → β}
(h : Function.LeftInverse j i)
:
theorem
Filter.tendsto_finset_preimage_atTop_atTop
{α : Type u_3}
{β : Type u_4}
{f : α → β}
(hf : Function.Injective f)
:
Filter.Tendsto (fun (s : Finset β) => s.preimage f ⋯) Filter.atTop Filter.atTop
theorem
Filter.tendsto_finset_prod_atTop
{ι : Type u_1}
{ι' : Type u_2}
:
Filter.Tendsto (fun (p : Finset ι × Finset ι') => p.1 ×ˢ p.2) Filter.atTop Filter.atTop
theorem
Filter.prod_map_atTop_eq
{α₁ : Type u_6}
{α₂ : Type u_7}
{β₁ : Type u_8}
{β₂ : Type u_9}
[Preorder β₁]
[Preorder β₂]
(u₁ : β₁ → α₁)
(u₂ : β₂ → α₂)
:
Filter.map u₁ Filter.atTop ×ˢ Filter.map u₂ Filter.atTop = Filter.map (Prod.map u₁ u₂) Filter.atTop
theorem
Filter.prod_map_atBot_eq
{α₁ : Type u_6}
{α₂ : Type u_7}
{β₁ : Type u_8}
{β₂ : Type u_9}
[Preorder β₁]
[Preorder β₂]
(u₁ : β₁ → α₁)
(u₂ : β₂ → α₂)
:
Filter.map u₁ Filter.atBot ×ˢ Filter.map u₂ Filter.atBot = Filter.map (Prod.map u₁ u₂) Filter.atBot
theorem
Filter.Tendsto.subseq_mem
{α : Type u_3}
{F : Filter α}
{V : ℕ → Set α}
(h : ∀ (n : ℕ), V n ∈ F)
{u : ℕ → α}
(hu : Filter.Tendsto u Filter.atTop F)
:
theorem
Filter.tendsto_atBot_diagonal
{α : Type u_3}
[Preorder α]
:
Filter.Tendsto (fun (a : α) => (a, a)) Filter.atBot Filter.atBot
theorem
Filter.tendsto_atTop_diagonal
{α : Type u_3}
[Preorder α]
:
Filter.Tendsto (fun (a : α) => (a, a)) Filter.atTop Filter.atTop
theorem
Filter.Tendsto.prod_map_prod_atBot
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder γ]
{F : Filter α}
{G : Filter β}
{f : α → γ}
{g : β → γ}
(hf : Filter.Tendsto f F Filter.atBot)
(hg : Filter.Tendsto g G Filter.atBot)
:
Filter.Tendsto (Prod.map f g) (F ×ˢ G) Filter.atBot
theorem
Filter.Tendsto.prod_map_prod_atTop
{α : Type u_3}
{β : Type u_4}
{γ : Type u_5}
[Preorder γ]
{F : Filter α}
{G : Filter β}
{f : α → γ}
{g : β → γ}
(hf : Filter.Tendsto f F Filter.atTop)
(hg : Filter.Tendsto g G Filter.atTop)
:
Filter.Tendsto (Prod.map f g) (F ×ˢ G) Filter.atTop
theorem
Filter.Tendsto.prod_atBot
{α : Type u_3}
{γ : Type u_5}
[Preorder α]
[Preorder γ]
{f g : α → γ}
(hf : Filter.Tendsto f Filter.atBot Filter.atBot)
(hg : Filter.Tendsto g Filter.atBot Filter.atBot)
:
theorem
Filter.Tendsto.prod_atTop
{α : Type u_3}
{γ : Type u_5}
[Preorder α]
[Preorder γ]
{f g : α → γ}
(hf : Filter.Tendsto f Filter.atTop Filter.atTop)
(hg : Filter.Tendsto g Filter.atTop Filter.atTop)
:
theorem
Filter.eventually_atBot_prod_self
{α : Type u_3}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{p : α × α → Prop}
:
(∀ᶠ (x : α × α) in Filter.atBot, p x) ↔ ∃ (a : α), ∀ (k l : α), k ≤ a → l ≤ a → p (k, l)
theorem
Filter.eventually_atTop_prod_self
{α : Type u_3}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{p : α × α → Prop}
:
(∀ᶠ (x : α × α) in Filter.atTop, p x) ↔ ∃ (a : α), ∀ (k l : α), a ≤ k → a ≤ l → p (k, l)
theorem
Filter.eventually_atBot_prod_self'
{α : Type u_3}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{p : α × α → Prop}
:
(∀ᶠ (x : α × α) in Filter.atBot, p x) ↔ ∃ (a : α), ∀ k ≤ a, ∀ l ≤ a, p (k, l)
theorem
Filter.eventually_atTop_prod_self'
{α : Type u_3}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{p : α × α → Prop}
:
(∀ᶠ (x : α × α) in Filter.atTop, p x) ↔ ∃ (a : α), ∀ k ≥ a, ∀ l ≥ a, p (k, l)
theorem
Filter.eventually_atTop_curry
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[Preorder β]
{p : α × β → Prop}
(hp : ∀ᶠ (x : α × β) in Filter.atTop, p x)
:
∀ᶠ (k : α) in Filter.atTop, ∀ᶠ (l : β) in Filter.atTop, p (k, l)
theorem
Filter.eventually_atBot_curry
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[Preorder β]
{p : α × β → Prop}
(hp : ∀ᶠ (x : α × β) in Filter.atBot, p x)
:
∀ᶠ (k : α) in Filter.atBot, ∀ᶠ (l : β) in Filter.atBot, p (k, l)
theorem
Filter.map_atTop_eq_of_gc_preorder
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[Preorder β]
[IsDirected β fun (x1 x2 : β) => x1 ≤ x2]
{f : α → β}
(hf : Monotone f)
(b : β)
(hgi : ∀ c ≥ b, ∃ (x : α), f x = c ∧ ∀ (a : α), f a ≤ c ↔ a ≤ x)
:
A function f maps upwards closed sets (atTop sets) to upwards closed sets when it is a
Galois insertion. The Galois "insertion" and "connection" is weakened to only require it to be an
insertion and a connection above b.
theorem
Filter.map_atTop_eq_of_gc
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[PartialOrder β]
[IsDirected β fun (x1 x2 : β) => x1 ≤ x2]
{f : α → β}
(g : β → α)
(b : β)
(hf : Monotone f)
(gc : ∀ (a : α), ∀ c ≥ b, f a ≤ c ↔ a ≤ g c)
(hgi : ∀ c ≥ b, c ≤ f (g c))
:
A function f maps upwards closed sets (atTop sets) to upwards closed sets when it is a
Galois insertion. The Galois "insertion" and "connection" is weakened to only require it to be an
insertion and a connection above b.
theorem
Filter.map_atBot_eq_of_gc_preorder
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[Preorder β]
[IsDirected β fun (x1 x2 : β) => x1 ≥ x2]
{f : α → β}
(hf : Monotone f)
(b : β)
(hgi : ∀ c ≤ b, ∃ (x : α), f x = c ∧ ∀ (a : α), c ≤ f a ↔ x ≤ a)
:
theorem
Filter.map_atBot_eq_of_gc
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[PartialOrder β]
[IsDirected β fun (x1 x2 : β) => x1 ≥ x2]
{f : α → β}
(g : β → α)
(b' : β)
(hf : Monotone f)
(gc : ∀ (a : α), ∀ b ≤ b', b ≤ f a ↔ g b ≤ a)
(hgi : ∀ b ≤ b', f (g b) ≤ b)
:
theorem
Filter.map_val_atTop_of_Ici_subset
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{a : α}
{s : Set α}
(h : Set.Ici a ⊆ s)
:
@[simp]
theorem
Filter.map_val_Ici_atTop
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
The image of the filter atTop on Ici a under the coercion equals atTop.
@[simp]
theorem
Filter.map_val_Ioi_atTop
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[NoMaxOrder α]
(a : α)
:
The image of the filter atTop on Ioi a under the coercion equals atTop.
theorem
Filter.atTop_Ioi_eq
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
The atTop filter for an open interval Ioi a comes from the atTop filter in the ambient
order.
theorem
Filter.atTop_Ici_eq
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
(a : α)
:
The atTop filter for an open interval Ici a comes from the atTop filter in the ambient
order.
@[simp]
theorem
Filter.map_val_Iio_atBot
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[NoMinOrder α]
(a : α)
:
The atBot filter for an open interval Iio a comes from the atBot filter in the ambient
order.
theorem
Filter.atBot_Iio_eq
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
(a : α)
:
The atBot filter for an open interval Iio a comes from the atBot filter in the ambient
order.
@[simp]
theorem
Filter.map_val_Iic_atBot
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
(a : α)
:
The atBot filter for an open interval Iic a comes from the atBot filter in the ambient
order.
theorem
Filter.atBot_Iic_eq
{α : Type u_3}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
(a : α)
:
The atBot filter for an open interval Iic a comes from the atBot filter in the ambient
order.
theorem
Filter.tendsto_Ioi_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{a : α}
{f : β → ↑(Set.Ioi a)}
{l : Filter β}
:
Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l Filter.atTop
theorem
Filter.tendsto_Iio_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{a : α}
{f : β → ↑(Set.Iio a)}
{l : Filter β}
:
Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l Filter.atBot
theorem
Filter.tendsto_Ici_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{a : α}
{f : β → ↑(Set.Ici a)}
{l : Filter β}
:
Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l Filter.atTop
theorem
Filter.tendsto_Iic_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{a : α}
{f : β → ↑(Set.Iic a)}
{l : Filter β}
:
Filter.Tendsto f l Filter.atBot ↔ Filter.Tendsto (fun (x : β) => ↑(f x)) l Filter.atBot
@[simp]
theorem
Filter.tendsto_comp_val_Ioi_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[NoMaxOrder α]
{a : α}
{f : α → β}
{l : Filter β}
:
Filter.Tendsto (fun (x : ↑(Set.Ioi a)) => f ↑x) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
@[simp]
theorem
Filter.tendsto_comp_val_Ici_atTop
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
{a : α}
{f : α → β}
{l : Filter β}
:
Filter.Tendsto (fun (x : ↑(Set.Ici a)) => f ↑x) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
@[simp]
theorem
Filter.tendsto_comp_val_Iio_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[NoMinOrder α]
{a : α}
{f : α → β}
{l : Filter β}
:
Filter.Tendsto (fun (x : ↑(Set.Iio a)) => f ↑x) Filter.atBot l ↔ Filter.Tendsto f Filter.atBot l
@[simp]
theorem
Filter.tendsto_comp_val_Iic_atBot
{α : Type u_3}
{β : Type u_4}
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
{a : α}
{f : α → β}
{l : Filter β}
:
Filter.Tendsto (fun (x : ↑(Set.Iic a)) => f ↑x) Filter.atBot l ↔ Filter.Tendsto f Filter.atBot l
theorem
Filter.map_add_atTop_eq_nat
(k : ℕ)
:
Filter.map (fun (a : ℕ) => a + k) Filter.atTop = Filter.atTop
theorem
Filter.map_sub_atTop_eq_nat
(k : ℕ)
:
Filter.map (fun (a : ℕ) => a - k) Filter.atTop = Filter.atTop
theorem
Filter.tendsto_add_atTop_nat
(k : ℕ)
:
Filter.Tendsto (fun (a : ℕ) => a + k) Filter.atTop Filter.atTop
theorem
Filter.tendsto_sub_atTop_nat
(k : ℕ)
:
Filter.Tendsto (fun (a : ℕ) => a - k) Filter.atTop Filter.atTop
theorem
Filter.tendsto_add_atTop_iff_nat
{α : Type u_3}
{f : ℕ → α}
{l : Filter α}
(k : ℕ)
:
Filter.Tendsto (fun (n : ℕ) => f (n + k)) Filter.atTop l ↔ Filter.Tendsto f Filter.atTop l
theorem
Filter.map_div_atTop_eq_nat
(k : ℕ)
(hk : 0 < k)
:
Filter.map (fun (a : ℕ) => a / k) Filter.atTop = Filter.atTop
theorem
Filter.unbounded_of_tendsto_atTop
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[Preorder β]
{f : α → β}
[NoMaxOrder β]
(h : Filter.Tendsto f Filter.atTop Filter.atTop)
:
theorem
Filter.unbounded_of_tendsto_atBot
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≤ x2]
[Preorder β]
{f : α → β}
[NoMinOrder β]
(h : Filter.Tendsto f Filter.atTop Filter.atBot)
:
theorem
Filter.unbounded_of_tendsto_atTop'
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[Preorder β]
{f : α → β}
[NoMaxOrder β]
(h : Filter.Tendsto f Filter.atBot Filter.atTop)
:
theorem
Filter.unbounded_of_tendsto_atBot'
{α : Type u_3}
{β : Type u_4}
[Nonempty α]
[Preorder α]
[IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
[Preorder β]
{f : α → β}
[NoMinOrder β]
(h : Filter.Tendsto f Filter.atBot Filter.atBot)
:
theorem
Filter.tendsto_atTop_of_monotone_of_filter
{ι : Type u_1}
{α : Type u_3}
[Preorder ι]
[Preorder α]
{l : Filter ι}
{u : ι → α}
(h : Monotone u)
[l.NeBot]
(hu : Filter.Tendsto u l Filter.atTop)
:
If a monotone function u : ι → α tends to atTop along some non-trivial filter l, then
it tends to atTop along atTop.
theorem
Filter.tendsto_atBot_of_monotone_of_filter
{ι : Type u_1}
{α : Type u_3}
[Preorder ι]
[Preorder α]
{l : Filter ι}
{u : ι → α}
(h : Monotone u)
[l.NeBot]
(hu : Filter.Tendsto u l Filter.atBot)
:
If a monotone function u : ι → α tends to atBot along some non-trivial filter l, then
it tends to atBot along atBot.
theorem
Filter.tendsto_atTop_of_monotone_of_subseq
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Preorder ι]
[Preorder α]
{u : ι → α}
{φ : ι' → ι}
(h : Monotone u)
{l : Filter ι'}
[l.NeBot]
(H : Filter.Tendsto (u ∘ φ) l Filter.atTop)
:
theorem
Filter.tendsto_atBot_of_monotone_of_subseq
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Preorder ι]
[Preorder α]
{u : ι → α}
{φ : ι' → ι}
(h : Monotone u)
{l : Filter ι'}
[l.NeBot]
(H : Filter.Tendsto (u ∘ φ) l Filter.atBot)
:
theorem
Filter.HasAntitoneBasis.comp_mono
{ι : Type u_1}
{ι' : Type u_2}
{α : Type u_3}
[Nonempty ι]
[Preorder ι]
[IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2]
[Preorder ι']
{l : Filter α}
{s : ι' → Set α}
(hs : l.HasAntitoneBasis s)
{φ : ι → ι'}
(φ_mono : Monotone φ)
(hφ : Filter.Tendsto φ Filter.atTop Filter.atTop)
:
l.HasAntitoneBasis (s ∘ φ)
theorem
Filter.HasAntitoneBasis.comp_strictMono
{α : Type u_3}
{l : Filter α}
{s : ℕ → Set α}
(hs : l.HasAntitoneBasis s)
{φ : ℕ → ℕ}
(hφ : StrictMono φ)
:
l.HasAntitoneBasis (s ∘ φ)
theorem
Filter.HasAntitoneBasis.subbasis_with_rel
{α : Type u_3}
{f : Filter α}
{s : ℕ → Set α}
(hs : f.HasAntitoneBasis s)
{r : ℕ → ℕ → Prop}
(hr : ∀ (m : ℕ), ∀ᶠ (n : ℕ) in Filter.atTop, r m n)
:
Given an antitone basis s : ℕ → Set α of a filter, extract an antitone subbasis s ∘ φ,
φ : ℕ → ℕ, such that m < n implies r (φ m) (φ n). This lemma can be used to extract an
antitone basis with basis sets decreasing "sufficiently fast".
theorem
Filter.subseq_forall_of_frequently
{ι : Type u_6}
{x : ℕ → ι}
{p : ι → Prop}
{l : Filter ι}
(h_tendsto : Filter.Tendsto x Filter.atTop l)
(h : ∃ᶠ (n : ℕ) in Filter.atTop, p (x n))
:
∃ (ns : ℕ → ℕ), Filter.Tendsto (fun (n : ℕ) => x (ns n)) Filter.atTop l ∧ ∀ (n : ℕ), p (x (ns n))
theorem
Monotone.piecewise_eventually_eq_iUnion
{ι : Type u_1}
{α : Type u_3}
{β : α → Type u_6}
[Preorder ι]
{s : ι → Set α}
[(i : ι) → DecidablePred fun (x : α) => x ∈ s i]
[DecidablePred fun (x : α) => x ∈ ⋃ (i : ι), s i]
(hs : Monotone s)
(f g : (a : α) → β a)
(a : α)
:
∀ᶠ (i : ι) in Filter.atTop, (s i).piecewise f g a = (⋃ (i : ι), s i).piecewise f g a
theorem
Antitone.piecewise_eventually_eq_iInter
{ι : Type u_1}
{α : Type u_3}
{β : α → Type u_6}
[Preorder ι]
{s : ι → Set α}
[(i : ι) → DecidablePred fun (x : α) => x ∈ s i]
[DecidablePred fun (x : α) => x ∈ ⋂ (i : ι), s i]
(hs : Antitone s)
(f g : (a : α) → β a)
(a : α)
:
∀ᶠ (i : ι) in Filter.atTop, (s i).piecewise f g a = (⋂ (i : ι), s i).piecewise f g a
theorem
Nat.eventually_pow_lt_factorial_sub
(c d : ℕ)
:
∀ᶠ (n : ℕ) in Filter.atTop, c ^ n < (n - d).factorial