star_lt_iff

Mathlib.Algebra.Order.Star.Basic

URI: https://scilib.ai/kg/mathlib#star_lt_iff

English

star x < y iff x < star y.

Русский

star x < y тогда и только тогда, когда x < star y.

LaTeX

$$$star\ x < y \iff x < star\ y$$$

Lean4

theorem star_lt_iff {x y : R} : star x < y ↔ x < star y := by rw [← star_lt_star_iff, star_star]

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

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

Разделы

Аффилиация

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