chainHeight_dual — Mathlib

English

Taking the dual (order reversal) preserves chainHeight: (ofDual⁻¹' s).chainHeight = s.chainHeight.

Русский

Переупорядочивание сохраняет цепную высоту: (ofDual⁻¹' s).chainHeight = s.chainHeight.

LaTeX

$$(\\mathrm{ofDual} \\!^{-1}' s).chainHeight = s.chainHeight$$

Lean4

@[simp]
theorem chainHeight_dual : (ofDual ⁻¹' s).chainHeight = s.chainHeight := by
  apply le_antisymm <;>
    · rw [chainHeight_le_chainHeight_iff]
      rintro l ⟨h₁, h₂⟩
      exact ⟨l.reverse, ⟨isChain_reverse.mpr h₁, fun i h ↦ h₂ i (mem_reverse.mp h)⟩, length_reverse.symm⟩

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