doc-next-gen

Mathlib.Logic.Small.Basic

Module docstring

{"# Instances and theorems for Small.

In particular we prove small_of_injective and small_of_surjective. ","We don't define Countable.toSmall in this file, to keep imports to Logic to a minimum. "}

small_subtype instance
(α : Type v) [Small.{w} α] (P : α → Prop) : Small.{w} { x // P x }
Full source 
instance small_subtype (α : Type v) [Small.{w} α] (P : α → Prop) : Small.{w} { x // P x } :=
  small_map (equivShrink α).subtypeEquivOfSubtype'
Subtypes of Small Types are Small
Informal description
For any $w$-small type $\alpha$ and any predicate $P$ on $\alpha$, the subtype $\{x \in \alpha \mid P(x)\}$ is also $w$-small.
small_of_injective theorem
{α : Type v} {β : Type w} [Small.{u} β] {f : α → β} (hf : Function.Injective f) : Small.{u} α
Full source 
theorem small_of_injective {α : Type v} {β : Type w} [Small.{u} β] {f : α → β}
    (hf : Function.Injective f) : Small.{u} α :=
  small_map (Equiv.ofInjective f hf)
Injectivity Preserves Smallness
Informal description
Let $\alpha$ and $\beta$ be types, with $\beta$ being $u$-small. If there exists an injective function $f \colon \alpha \to \beta$, then $\alpha$ is also $u$-small.
small_of_surjective theorem
{α : Type v} {β : Type w} [Small.{u} α] {f : α → β} (hf : Function.Surjective f) : Small.{u} β
Full source 
theorem small_of_surjective {α : Type v} {β : Type w} [Small.{u} α] {f : α → β}
    (hf : Function.Surjective f) : Small.{u} β :=
  small_of_injective (Function.injective_surjInv hf)
Surjectivity Preserves Smallness
Informal description
Let $\alpha$ and $\beta$ be types, with $\alpha$ being $u$-small. If there exists a surjective function $f \colon \alpha \to \beta$, then $\beta$ is also $u$-small.
small_of_injective_of_exists theorem
{α : Type v} {β : Type w} {γ : Type v'} [Small.{u} α] (f : α → γ) {g : β → γ} (hg : Function.Injective g) (h : ∀ b : β, ∃ a : α, f a = g b) : Small.{u} β
Full source 
/-- This can be seen as a version of `small_of_surjective` in which the function `f` doesn't
actually land in `β` but in some larger type `γ` related to `β` via an injective function `g`.
-/
theorem small_of_injective_of_exists {α : Type v} {β : Type w} {γ : Type v'} [Small.{u} α]
    (f : α → γ) {g : β → γ} (hg : Function.Injective g) (h : ∀ b : β, ∃ a : α, f a = g b) :
    Small.{u} β := by
  by_cases hβ : Nonempty β
  · refine small_of_surjective (f := Function.invFunFunction.invFun g ∘ f) (fun b => ?_)
    obtain ⟨a, ha⟩ := h b
    exact ⟨a, by rw [Function.comp_apply, ha, Function.leftInverse_invFun hg]⟩
  · simp only [not_nonempty_iff] at hβ
    infer_instance
Smallness via Partial Surjection and Injection
Informal description
Let $\alpha$, $\beta$, and $\gamma$ be types, with $\alpha$ being $u$-small. Given functions $f \colon \alpha \to \gamma$ and $g \colon \beta \to \gamma$ such that $g$ is injective, and for every $b \in \beta$ there exists $a \in \alpha$ with $f(a) = g(b)$, then $\beta$ is also $u$-small.
small_Pi instance
{α} (β : α → Type*) [Small.{w} α] [∀ a, Small.{w} (β a)] : Small.{w} (∀ a, β a)
Full source 
instance small_Pi {α} (β : α → Type*) [Small.{w} α] [∀ a, Small.{w} (β a)] :
    Small.{w} (∀ a, β a) :=
  ⟨⟨∀ a' : Shrink α, Shrink (β ((equivShrink α).symm a')),
      ⟨Equiv.piCongr (equivShrink α) fun a => by simpa using equivShrink (β a)⟩⟩⟩
Smallness of Dependent Product Types
Informal description
For any type family $\beta : \alpha \to \text{Type}^*$ where both $\alpha$ and each $\beta(a)$ are $w$-small, the dependent product type $\prod_{a : \alpha} \beta(a)$ is also $w$-small.