ofDual_preimage_latticeClosure — Mathlib

English

The preimage under the order dual map commutes with latticeClosure.

Русский

Предобраз под отображением двойственной порядка сохраняет latticeClosure.

LaTeX

$$$\operatorname{ofDual}^{-1} \; \mathrm{latticeClosure}(s) = \mathrm{latticeClosure}(\operatorname{ofDual}^{-1} s)$$$

Lean4

theorem ofDual_preimage_latticeClosure (s : Set α) : ofDual ⁻¹' latticeClosure s = latticeClosure (ofDual ⁻¹' s) :=
  by
  change ClosureOperator.ofCompletePred _ _ _ = ClosureOperator.ofCompletePred _ _ _
  congr 2
  ext
  exact ⟨fun h => ⟨h.2, h.1⟩, fun h => ⟨h.2, h.1⟩⟩

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