dual_ordSeparatingSet — Mathlib

English

ordSeparatingSet (ofDual^{-1} s) (ofDual^{-1} t) = ofDual^{-1} (ordSeparatingSet s t).

Русский

ordSeparatingSet в двойственной перестановке равен образу ordSeparatingSet s t под двойственным отображением.

LaTeX

$$ordSeparatingSet (ofDual^{-1} \,' s) (ofDual^{-1} t) = ofDual^{-1} (ordSeparatingSet s t)$$

Lean4

theorem dual_ordSeparatingSet : ordSeparatingSet (ofDual ⁻¹' s) (ofDual ⁻¹' t) = ofDual ⁻¹' ordSeparatingSet s t := by
  simp only [ordSeparatingSet, mem_preimage, ← toDual.surjective.iUnion_comp, ofDual_toDual, dual_ordConnectedComponent,
    ← preimage_compl, preimage_inter, preimage_iUnion]

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