mem_inf

Mathlib.Geometry.Convex.Cone.Basic

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

English

For any x and cones C1, C2, x ∈ C1 ⊓ C2 iff x ∈ C1 and x ∈ C2.

Русский

Для любых конусов C1, C2 и вектора x верно: x ∈ C1 ⊓ C2 тогда и только если x ∈ C1 и x ∈ C2.

LaTeX

$$x ∈ C1 ⊓ C2 ↔ x ∈ C1 ∧ x ∈ C2$$

Lean4

@[simp]
theorem mem_inf : x ∈ C₁ ⊓ C₂ ↔ x ∈ C₁ ∧ x ∈ C₂ :=
  .rfl

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

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

Разделы

Аффилиация

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