map_symm_eq_iff_eq_map — Mathlib

English

For an order isomorphism e: β ≃o α, the equality L.map e.symm = M is equivalent to L = M.map e.

Русский

Для порядкового изоморфизма e: β ≃o α равенство L.map e.symm = M эквивалентно L = M.map e.

LaTeX

$$L.map e.symm = M ↔ L = M.map e$$

Lean4

theorem map_symm_eq_iff_eq_map {M : Sublattice β} {e : β ≃o α} : L.map ↑e.symm = M ↔ L = M.map ↑e := by
  simp_rw [← coe_inj]; exact (Equiv.eq_image_iff_symm_image_eq _ _ _).symm

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