mem_cylinder_comm

Mathlib.Topology.MetricSpace.PiNat

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

English

For x,y and n, y ∈ cylinder x n iff x ∈ cylinder y n.

Русский

Для x,y и n выполняется: y ∈ cylinder(x,n) ⇔ x ∈ cylinder(y,n).

LaTeX

$$$y \\in \\mathrm{cylinder}(x,n) \\iff x \\in \\mathrm{cylinder}(y,n)$$$

Lean4

theorem mem_cylinder_comm (x y : ∀ n, E n) (n : ℕ) : y ∈ cylinder x n ↔ x ∈ cylinder y n := by simp [eq_comm]

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

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

Разделы

Аффилиация

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