setSeq_mono

Mathlib.Topology.UniformSpace.Cauchy

URI: https://scilib.ai/kg/mathlib#SequentiallyComplete.setSeq_mono

English

If m ≤ n then setSeq(n) ⊆ setSeq(m).

Русский

Если m ≤ n, то setSeq(n) ⊆ setSeq(m).

LaTeX

$$$m \le n \Rightarrow setSeq(hf,U_{mem})(n) \subseteq setSeq(hf,U_{mem})(m)$$$

Lean4

theorem setSeq_mono ⦃m n : ℕ⦄ (h : m ≤ n) : setSeq hf U_mem n ⊆ setSeq hf U_mem m :=
  biInter_subset_biInter_left <| Iic_subset_Iic.2 h

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru