English
Let P be a preorder and 𝒟 : ι → Cofinal P a family of cofinal subsets indexed by a countable set. Then the sequence n ↦ sequenceOfCofinals p 𝒟 n is monotone in n, i.e., if n ≤ m then sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 m.
Русский
Пусть P — упорядочение, 𝒟 : ι → Cofinal P — семейство кофинальных подмножеств, индексируемое счётной множестю. Тогда последовательность n ↦ sequenceOfCofinals p 𝒟 n монотонна по n, т.е. n ≤ m ⇒ sequenceOfCofinals p 𝒟 n ≤ sequenceOfCofinals p 𝒟 m.
LaTeX
$$$\\forall n \\; (n \\le m) \\Rightarrow sequenceOfCofinals\\, p\\, 𝒟\\; n \\le sequenceOfCofinals\\, p\\, 𝒟\\; m$$$
Lean4
theorem monotone : Monotone (sequenceOfCofinals p 𝒟) :=
by
apply monotone_nat_of_le_succ
intro n
dsimp only [sequenceOfCofinals, Nat.add]
cases (Encodable.decode n : Option ι)
· rfl
· apply Cofinal.le_above
