mem_mk

Mathlib.Geometry.Convex.Cone.Basic

URI: https://scilib.ai/kg/mathlib#ConvexCone.mem_mk

English

Membership in mk s h1 h2 is equivalent to membership in s.

Русский

Принадлежность к mk s равна принадлежности к s.

LaTeX

$$$ x \\in mk(R := R) s h_1 h_2 \\iff x \\in s$$$

Lean4

@[simp]
theorem mem_mk {h₁ h₂} : x ∈ mk (R := R) s h₁ h₂ ↔ x ∈ s :=
  .rfl

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

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

Разделы

Аффилиация

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