cylinder_anti

Mathlib.Topology.MetricSpace.PiNat

URI: https://scilib.ai/kg/mathlib#PiNat.cylinder_anti

English

If m ≤ n, then cylinder x n ⊆ cylinder x m.

Русский

Если m ≤ n, то цилиндр x n ⊆ цилиндр x m.

LaTeX

$$$\\text{If } m \\le n:\\;\\ \\mathrm{cylinder}(x,n) \\subseteq \\mathrm{cylinder}(x,m)$$$

Lean4

theorem cylinder_anti (x : ∀ n, E n) {m n : ℕ} (h : m ≤ n) : cylinder x n ⊆ cylinder x m := fun _y hy i hi =>
  hy i (hi.trans_le h)

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

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

Разделы

Аффилиация

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