seq_pair_mem

Mathlib.Topology.UniformSpace.Cauchy

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

← MathLib Explorer

English

For given N ≤ m and N ≤ n, the pair (seq(m), seq(n)) belongs to U(N).

Русский

Для данного N ≤ m и N ≤ n пара (seq(m), seq(n)) принадлежит U(N).

LaTeX

$$$(\text{seq}(hf,U_{mem},m), \text{seq}(hf,U_{mem},n)) \in U(N)$$$

Lean4

theorem seq_pair_mem ⦃N m n : ℕ⦄ (hm : N ≤ m) (hn : N ≤ n) : (seq hf U_mem m, seq hf U_mem n) ∈ U N :=
  setSeq_prod_subset hf U_mem hm hn ⟨seq_mem hf U_mem m, seq_mem hf U_mem n⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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