Filter.atTop and Filter.atBot in (conditionally) complete lattices

theorem Filter.Subsingleton.atTop_eq (α : Type u_6) [Subsingleton α] [Preorder α] : atTop = ⊤

theorem Filter.Subsingleton.atBot_eq (α : Type u_6) [Subsingleton α] [Preorder α] : atBot = ⊤

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.