English
There exists an index i such that for every j, there is an injection β(i) ↪ β(j).
Русский
Существует индекс i, для которого для каждого j существует инъекция β(i) ↪ β(j).
LaTeX
$$$\exists i, \forall j, β(i) \hookrightarrow β(j)$$$
Lean4
/-- The cardinals are well-ordered. We express it here by the fact that in any set of cardinals
there is an element that injects into the others.
See `Cardinal.conditionallyCompleteLinearOrderBot` for (one of) the lattice instances. -/
theorem min_injective [I : Nonempty ι] : ∃ i, Nonempty (∀ j, β i ↪ β j) :=
let ⟨s, hs⟩ :=
show ∃ s, Maximal (· ∈ sets β) s
by
refine
zorn_subset _ fun c hc hcc ↦ ⟨⋃₀ c, fun i x ⟨p, hpc, hxp⟩ y ⟨q, hqc, hyq⟩ hi ↦ ?_, fun _ ↦ subset_sUnion_of_mem⟩
exact (hcc.total hpc hqc).elim (fun h ↦ hc hqc i (h hxp) hyq hi) fun h ↦ hc hpc i hxp (h hyq) hi
let ⟨i, e⟩ :=
show ∃ i, Surjective fun x : s => x.val i from
Classical.by_contradiction fun h =>
have h : ∀ i, ∃ y, ∀ x ∈ s, (x : ∀ i, β i) i ≠ y := by simpa [Surjective] using h
let ⟨f, hf⟩ := Classical.axiom_of_choice h
have : f ∈ s :=
have : insert f s ∈ sets β := fun i x hx y hy =>
by
rcases hx with hx | hx <;> rcases hy with hy | hy; · simp [hx, hy]
· subst x
exact fun e => (hf i y hy e.symm).elim
· subst y
exact fun e => (hf i x hx e).elim
· exact hs.prop i hx hy
hs.eq_of_subset this (subset_insert _ _) ▸ mem_insert ..
let ⟨i⟩ := I
hf i f this rfl
⟨i, ⟨fun j => ⟨s.restrict (fun x => x j) ∘ surjInv e, ((hs.1 j).injective).comp (injective_surjInv _)⟩⟩⟩
