C1_projOrd — Mathlib

English

Let x belong to the C1 class with respect to the order, then applying the projection and the swap operation recovers x exactly.

Русский

Пусть x принадлежит классу C1 по отношению, тогда после применения проекции и перестановки значений мы получаем x обратно.

LaTeX

$$$ x \\in C_1 C ho \\Rightarrow \\mathrm{SwapTrue}(o, \\mathrm{Proj}(\\operatorname{ord} I \\cdot < o)\\, x) = x $$$

Lean4

theorem C1_projOrd {x : I → Bool} (hx : x ∈ C1 C ho) : SwapTrue o (Proj (ord I · < o) x) = x :=
  by
  ext i
  dsimp [SwapTrue, Proj]
  split_ifs with hi h
  · rw [ord_term ho] at hi
    rw [← hx.2, hi]
  · rfl
  · simp only [not_lt] at h
    have h' : o < ord I i := lt_of_le_of_ne h (Ne.symm hi)
    specialize hsC x hx.1 i
    rw [← not_imp_not] at hsC
    simp only [not_lt, Bool.not_eq_true, Order.succ_le_iff] at hsC
    exact (hsC h').symm

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