English
For any CauSeq f, exactly one of Pos f, LimZero f, or Pos(-f) holds.
Русский
Для любой Каус-секвенции f верно ровно одно из: Pos f, LimZero f или Pos(-f).
LaTeX
$$$ \text{Pos}(f) \lor \text{LimZero}(f) \lor \text{Pos}(-f) $$$
Lean4
theorem trichotomy (f : CauSeq α abs) : Pos f ∨ LimZero f ∨ Pos (-f) :=
by
rcases Classical.em (LimZero f) with h | h
· simp [*]
simp only [false_or, h]
rcases abv_pos_of_not_limZero h with ⟨K, K0, hK⟩
rcases exists_forall_ge_and hK (f.cauchy₃ K0) with ⟨i, hi⟩
refine (le_total 0 (f i)).imp ?_ ?_ <;> refine fun h => ⟨K, K0, i, fun j ij => ?_⟩ <;> have := (hi _ ij).1 <;>
obtain ⟨h₁, h₂⟩ := hi _ le_rfl
· rwa [abs_of_nonneg] at this
rw [abs_of_nonneg h] at h₁
exact (le_add_iff_nonneg_right _).1 (le_trans h₁ <| neg_le_sub_iff_le_add'.1 <| le_of_lt (abs_lt.1 <| h₂ _ ij).1)
· rwa [abs_of_nonpos] at this
rw [abs_of_nonpos h] at h₁
rw [← sub_le_sub_iff_right, zero_sub]
exact le_trans (le_of_lt (abs_lt.1 <| h₂ _ ij).2) h₁
