English
The full subcategory (cofilteredClosure f).FullSubcategory is small.
Русский
Полная подпредкатегория (cofilteredClosure f).FullSubcategory является малой.
LaTeX
$$$\\mathrm{Small}((\\mathrm{cofilteredClosure} f).\\mathrm{FullSubcategory})$$$
Lean4
theorem small_fullSubcategory_cofilteredClosure : Small.{max v w} (cofilteredClosure f).FullSubcategory :=
by
refine
small_of_injective_of_exists (CofilteredClosureSmall.abstractCofilteredClosureRealization f)
(fun _ _ => ObjectProperty.FullSubcategory.ext) ?_
rintro ⟨j, h⟩
induction h with
| base x =>
refine ⟨⟨0, ?_⟩, ?_⟩
· simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
exact ULift.up x
· simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
rfl
| min hj₁ hj₂ ih ih' =>
rcases ih with ⟨⟨n, x⟩, rfl⟩
rcases ih' with ⟨⟨m, y⟩, rfl⟩
refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
· simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
refine CofilteredClosureSmall.InductiveStep.min ?_ ?_ x y
all_goals apply Nat.lt_succ_of_le
exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
· simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
rfl
| eq hj₁ hj₂ g g' ih ih' =>
rcases ih with ⟨⟨n, x⟩, rfl⟩
rcases ih' with ⟨⟨m, y⟩, rfl⟩
refine ⟨⟨(Max.max n m).succ, ?_⟩, ?_⟩
· simp only [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
refine CofilteredClosureSmall.InductiveStep.eq ?_ ?_ x y g g'
all_goals apply Nat.lt_succ_of_le
exacts [Nat.le_max_left _ _, Nat.le_max_right _ _]
· simp only [CofilteredClosureSmall.abstractCofilteredClosureRealization]
rw! [CofilteredClosureSmall.bundledAbstractCofilteredClosure]
rfl
