dual_ordConnectedSection — Mathlib

English

The connected section commutes with dual preimages: ordConnectedSection(ofDual^{-1}'s s) = ofDual^{-1}' ordConnectedSection s.

Русский

Связанная секция коммутирует с обрязанными предобразами двойственного порядка: ordConnectedSection(ofDual^{-1}' s) = ofDual^{-1}' ordConnectedSection s.

LaTeX

$$$\operatorname{ordConnectedSection}(\text{ofDual}^{-1}' s) = \text{ofDual}^{-1}' \operatorname{ordConnectedSection}(s)$$$

Lean4

theorem dual_ordConnectedSection (s : Set α) : ordConnectedSection (ofDual ⁻¹' s) = ofDual ⁻¹' ordConnectedSection s :=
  by
  simp only [ordConnectedSection]
  simp +unfoldPartialApp only [ordConnectedProj]
  ext x
  simp only [mem_range, Subtype.exists, mem_preimage, OrderDual.exists, dual_ordConnectedComponent, ofDual_toDual]
  tauto

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