notConvergentSeq_antitone — Mathlib

English

The map j ↦ notConvergentSeq(f,g,n,j) is an antitone family in j; as j increases, the set becomes larger or equal.

Русский

Отображение j ↦ notConvergentSeq(f,g,n,j) антиупорядочено по возрастанию j; по мере увеличения j множество растёт или не уменьшается.

LaTeX

$$$\text{Antitone}(\,notConvergentSeq(f,g,n)\,)$$$

Lean4

theorem notConvergentSeq_antitone [Preorder ι] : Antitone (notConvergentSeq f g n) := fun _ _ hjk =>
  Set.iUnion₂_mono' fun l hl => ⟨l, le_trans hjk hl, Set.Subset.rfl⟩

Похожие утверждения