mem_Icc

Mathlib.Algebra.Order.Star.Basic

URI: https://scilib.ai/kg/mathlib#IsStarProjection.mem_Icc

← MathLib Explorer

English

For a star projection p, we have p ∈ [0,1].

Русский

Для star-проекции p имеет место p ∈ [0,1].

LaTeX

$$$ p \in [0,1] $$$

Lean4

/-- For a star projection `p`, we have `0 ≤ p ≤ 1`. -/
theorem mem_Icc (hp : IsStarProjection p) : p ∈ Set.Icc (0 : R) 1 := by
  simp only [Set.mem_Icc, hp.nonneg, hp.le_one, and_self]

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

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

Разделы

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

Аффилиация

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