English
An initial segment embedding is either surjective or its image is a principal segment: there exists b with ∀ x, x ∈ range f ↔ s x b.
Русский
Начальное отображение сегмента либо сюръективно, либо его образ является принципиальным сегментом: существует b, такое что ∀ x, x прó Range f эквивалентно s x b.
LaTeX
$$$[IsWellOrder \\ β \\ s] (f : r \\preccurlyeq_i s) \\\\Rightarrow (Surjective f) \\\\lor \\\\ Exists b, \\\\forall x, x \\in\\mathrm{range}(f) \\leftrightarrow s x b.$$$
Lean4
/-- An initial segment embedding is either an isomorphism, or a principal segment embedding.
See also `InitialSeg.ltOrEq`. -/
theorem eq_or_principal [IsWellOrder β s] (f : r ≼i s) : Surjective f ∨ ∃ b, ∀ x, x ∈ Set.range f ↔ s x b :=
by
apply or_iff_not_imp_right.2
intro h b
push_neg at h
apply IsWellFounded.induction s b
intro x IH
obtain ⟨y, ⟨hy, hs⟩ | ⟨hy, hs⟩⟩ := h x
· obtain (rfl | h) := (trichotomous y x).resolve_left hs
· exact hy
· obtain ⟨z, rfl⟩ := hy
exact f.mem_range_of_rel h
· obtain ⟨z, rfl⟩ := IH y hs
cases hy (Set.mem_range_self z)
