doc-next-gen

Mathlib.Order.Filter.AtTopBot.Finset

Module docstring

{"# Filter.atTop and Filter.atBot filters and finite sets. "}

Filter.atTop_finset_eq_iInf theorem
: (atTop : Filter (Finset α)) = ⨅ x : α, 𝓟 (Ici { x })
Full source 
theorem atTop_finset_eq_iInf : (atTop : Filter (Finset α)) = ⨅ x : α, 𝓟 (Ici {x}) := by
  refine le_antisymm (le_iInf fun i => le_principal_iff.2 <| mem_atTop ({i} : Finset α)) ?_
  refine
    le_iInf fun s =>
      le_principal_iff.2 <| mem_iInf_of_iInter s.finite_toSet (fun i => mem_principal_self _) ?_
  simp only [subset_def, mem_iInter, SetCoe.forall, mem_Ici, Finset.le_iff_subset,
    Finset.mem_singleton, Finset.subset_iff, forall_eq]
  exact fun t => id
Characterization of `atTop` Filter on Finite Sets as Infimum of Principal Filters
Informal description
The filter `atTop` on the type of finite sets `Finset α` is equal to the infimum over all elements `x : α` of the principal filter generated by the left-closed right-infinite interval `[ {x}, ∞ )` in the finite sets. In other words: \[ \text{atTop} = \bigsqcap_{x \in \alpha} \mathcal{P}([ \{x\}, \infty)) \] where $\mathcal{P}(S)$ denotes the principal filter generated by the set $S$.
Filter.tendsto_atTop_finset_of_monotone theorem
[Preorder β] {f : β → Finset α} (h : Monotone f) (h' : ∀ x : α, ∃ n, x ∈ f n) : Tendsto f atTop atTop
Full source 
/-- If `f` is a monotone sequence of `Finset`s and each `x` belongs to one of `f n`, then
`Tendsto f atTop atTop`. -/
theorem tendsto_atTop_finset_of_monotone [Preorder β] {f : β → Finset α} (h : Monotone f)
    (h' : ∀ x : α, ∃ n, x ∈ f n) : Tendsto f atTop atTop := by
  simp only [atTop_finset_eq_iInf, tendsto_iInf, tendsto_principal]
  intro a
  rcases h' a with ⟨b, hb⟩
  exact (eventually_ge_atTop b).mono fun b' hb' => (Finset.singleton_subset_iff.2 hb).trans (h hb')
Monotone Sequence of Finite Sets Tends to Infinity if Exhaustive
Informal description
Let $\beta$ be a preorder and $f : \beta \to \mathrm{Finset}\,\alpha$ be a monotone function. If for every $x \in \alpha$ there exists $n \in \beta$ such that $x \in f(n)$, then the function $f$ tends to infinity in the `atTop` filter on $\beta$ and the `atTop` filter on $\mathrm{Finset}\,\alpha$. In other words, $f(n) \to \infty$ as $n \to \infty$.
Filter.tendsto_finset_image_atTop_atTop theorem
[DecidableEq β] {i : β → γ} {j : γ → β} (h : Function.LeftInverse j i) : Tendsto (Finset.image j) atTop atTop
Full source 
theorem tendsto_finset_image_atTop_atTop [DecidableEq β] {i : β → γ} {j : γ → β}
    (h : Function.LeftInverse j i) : Tendsto (Finset.image j) atTop atTop :=
  (Finset.image_mono j).tendsto_atTop_finset fun a =>
    ⟨{i a}, by simp only [Finset.image_singleton, h a, Finset.mem_singleton]⟩
Image of Finite Sets Under Left Inverse Preserves Tendency to Infinity
Informal description
Let $\beta$ and $\gamma$ be types with $\beta$ having decidable equality. Given functions $i : \beta \to \gamma$ and $j : \gamma \to \beta$ such that $j$ is a left inverse of $i$ (i.e., $j \circ i = \text{id}_\beta$), then the mapping of finite sets under $j$, $Finset.image\ j : Finset\ \gamma \to Finset\ \beta$, tends to infinity in the `atTop` filter. That is, as the input finite set in $Finset\ \gamma$ grows without bound, its image under $j$ in $Finset\ \beta$ also grows without bound.
Filter.tendsto_finset_preimage_atTop_atTop theorem
{f : α → β} (hf : Function.Injective f) : Tendsto (fun s : Finset β => s.preimage f (hf.injOn)) atTop atTop
Full source 
theorem tendsto_finset_preimage_atTop_atTop {f : α → β} (hf : Function.Injective f) :
    Tendsto (fun s : Finset β => s.preimage f (hf.injOn)) atTop atTop :=
  (Finset.monotone_preimage hf).tendsto_atTop_finset fun x =>
    ⟨{f x}, Finset.mem_preimage.2 <| Finset.mem_singleton_self _⟩
Preimage under Injective Function Preserves `atTop` Filter on Finite Sets
Informal description
For any injective function $f : \alpha \to \beta$, the preimage operation $s \mapsto f^{-1}(s)$ (where $s$ is a finite subset of $\beta$) preserves the `atTop` filter. That is, as $s$ grows without bound in $\beta$, its preimage $f^{-1}(s)$ also grows without bound in $\alpha$.
Filter.tendsto_toLeft_atTop theorem
: Tendsto (Finset.toLeft (α := α) (β := β)) atTop atTop
Full source 
lemma tendsto_toLeft_atTop :
    Tendsto (Finset.toLeft (α := α) (β := β)) atTop atTop := by
  intro s hs
  simp only [mem_atTop_sets, Finset.le_eq_subset, Filter.mem_map, Set.mem_preimage] at hs ⊢
  obtain ⟨t, H⟩ := hs
  exact ⟨t.disjSum ∅, fun b hb ↦ H _ (by simpa [← Finset.coe_subset, Set.subset_def] using hb)⟩
Left Injection Mapping Tends to Infinity in `atTop` Filter
Informal description
The function `Finset.toLeft`, which maps a finite set of elements of type $\alpha \oplus \beta$ to the corresponding finite set of left injections from $\alpha$, tends to infinity in the `atTop` filter. That is, as the input finite set grows without bound (in the `atTop` filter), the output finite set of left injections also grows without bound.
Filter.tendsto_toRight_atTop theorem
: Tendsto (Finset.toRight (α := α) (β := β)) atTop atTop
Full source 
lemma tendsto_toRight_atTop :
    Tendsto (Finset.toRight (α := α) (β := β)) atTop atTop := by
  intro s hs
  simp only [mem_atTop_sets, Finset.le_eq_subset, Filter.mem_map, Set.mem_preimage] at hs ⊢
  obtain ⟨t, H⟩ := hs
  exact ⟨.disjSum ∅ t, fun b hb ↦ H _ (by simpa [← Finset.coe_subset, Set.subset_def] using hb)⟩
Right Projection Preserves the `atTop` Filter on Finite Subsets of a Sum Type
Informal description
The function `Finset.toRight`, which maps finite subsets of $\alpha \oplus \beta$ to their right components (i.e., subsets of $\beta$), tends to infinity as its input tends to infinity. More precisely, the map $s \mapsto \mathrm{toRight}(s)$ is a filter-preserving function from the filter `atTop` on finite subsets of $\alpha \oplus \beta$ to the filter `atTop` on finite subsets of $\beta$.