setSeq_sub_aux

Mathlib.Topology.UniformSpace.Cauchy

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

English

For every n, setSeq(n) ⊆ setSeqAux(n).

Русский

Для каждого n множество setSeq(n) ⊆ setSeqAux(n).

LaTeX

$$$\text{setSeq}(n) \subseteq (\text{setSeqAux}(n)).$$$

Lean4

theorem setSeq_sub_aux (n : ℕ) : setSeq hf U_mem n ⊆ setSeqAux hf U_mem n :=
  biInter_subset_of_mem right_mem_Iic

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

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

Разделы

Аффилиация

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