Theorems · Theorem · logic and foundations

small_of_injective_of_exists

∀ {α : Type v} {β : Type w} {γ : Type v'} [Small.{u, v} α] (f : α → γ) {g : β → γ},
  Function.Injective g → (∀ (b : β), ∃ a, f a = g b) → Small.{u, w} β

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.

Defined in

Mathlib.Logic.Small.Basic

Cited by

2 results in Mathlib

Foundations

Depth 24 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Small