rfl

Mathlib.Analysis.Convex.Visible

URI: https://scilib.ai/kg/mathlib#IsVisible.rfl

English

For any set s and any point x, x sees x through s.

Русский

Для любого множества s и любой точки x, x видит себя через s.

LaTeX

$$IsVisible 𝕜 s x x$$

Lean4

@[simp, refl]
theorem rfl : IsVisible 𝕜 s x x := by simp [IsVisible]

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

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

Разделы

Аффилиация

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