English
For any real x, applying symmetry to the projection to the unit interval equals the projection of 1 − x.
Русский
Для любого действительного x применение симметрии к проекции на единичный интервал равно проекции 1 − x.
LaTeX
$$$$ \sigma(\operatorname{projIcc}(0,1,0\le1\,x)) = \operatorname{projIcc}(0,1,0\le1\,(1-x)). $$$$
Lean4
@[simp]
theorem symm_projIcc (x : ℝ) : symm (projIcc 0 1 zero_le_one x) = projIcc 0 1 zero_le_one (1 - x) :=
by
ext
rcases le_total x 0 with h₀ | h₀
· simp [projIcc_of_le_left, projIcc_of_right_le, h₀]
· rcases le_total x 1 with h₁ | h₁
· lift x to I using ⟨h₀, h₁⟩
simp_rw [← coe_symm_eq, projIcc_val]
· simp [projIcc_of_le_left, projIcc_of_right_le, h₁]
