map_sSup_eq_sSup_symm_preimage — Mathlib

English

If f is an order isomorphism between complete lattices α ≃o β and s ⊆ α, then f( sup s ) equals the supremum in β of the preimage of s under f.symm.

Русский

Пусть f — упорядоченный изоморфизм между полными решётками α и β, и s ⊆ α. Тогда f( sup s ) равно супремуму по β множества, полученного как предобразное множество s под f.symm.

LaTeX

$$$$ f( \\mathrm{sup}\, s ) = \\mathrm{sup}( f^{-1}[s] ) $$$$

Lean4

theorem map_sSup_eq_sSup_symm_preimage [CompleteLattice β] (f : α ≃o β) (s : Set α) :
    f (sSup s) = sSup (f.symm ⁻¹' s) := by rw [map_sSup, ← sSup_image, f.image_eq_preimage]

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