map_sInf_eq_sInf_symm_preimage — Mathlib

English

If f is an order isomorphism f : α ≃o β and s ⊆ α, then f( inf s ) equals the infimum in β of the preimage of s under f.symm.

Русский

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

LaTeX

$$$$ f( \\inf s ) = \\inf( f.symm^{-1}[s] ) $$$$

Lean4

theorem map_sInf_eq_sInf_symm_preimage [CompleteLattice β] (f : α ≃o β) (s : Set α) :
    f (sInf s) = sInf (f.symm ⁻¹' s) := by
  rw [map_sInf, ← sInf_image, f.image_eq_preimage]
    /-
    ### iSup and iInf under set constructions
    -/

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