lt_symm_comm

Mathlib.Topology.UnitInterval

URI: https://scilib.ai/kg/mathlib#unitInterval.lt_symm_comm

English

For i,j ∈ I, i < σ(j) ⇔ σ(j) > i, i.e. i < 1 − j ⇔ 1 − j > i.

Русский

Для i,j ∈ I, i < σ(j) эквивалентно σ(j) > i, то есть i < 1 − j ⇔ 1 − j > i.

LaTeX

$$$\forall i,j\in I,\ i<\sigma(j) \iff \sigma(j) > i$$$

Lean4

theorem lt_symm_comm {i j : I} : i < σ j ↔ j < σ i := by rw [← symm_lt_symm, symm_symm]

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

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

Разделы

Аффилиация

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