isSublattice_preimage_toDual — Mathlib

English

IsSublattice of the preimage under toDual is equivalent to IsSublattice of the original set.

Русский

Субрешетка прообраза через toDual эквивалентна субрешетке исходного множества.

LaTeX

$$IsSublattice (toDual^{-1}' s) ↔ IsSublattice s$$

Lean4

@[simp]
theorem isSublattice_preimage_toDual {s : Set αᵒᵈ} : IsSublattice (toDual ⁻¹' s) ↔ IsSublattice s :=
  ⟨fun h ↦ ⟨h.2, h.1⟩, fun h ↦ ⟨h.2, h.1⟩⟩

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