symm_eq_zero

Mathlib.Topology.UnitInterval

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

English

For i ∈ I, σ(i) = 0 iff i = 1.

Русский

Для i ∈ I верно: σ(i) = 0 тогда и только тогда, когда i = 1.

LaTeX

$$$\sigma(i)=0 \iff i=1$$$

Lean4

@[simp]
theorem symm_eq_zero {i : I} : σ i = 0 ↔ i = 1 := by rw [← symm_one, symm_inj]

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

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

Разделы

Аффилиация

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