From aeee10d43f92ed128761e54778991e0c07c4108b Mon Sep 17 00:00:00 2001 From: Bergschaf Date: Wed, 29 Apr 2026 23:10:19 +0200 Subject: [PATCH 1/2] LatticeHom range --- Mathlib/Order/Sublattice.lean | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/Mathlib/Order/Sublattice.lean b/Mathlib/Order/Sublattice.lean index f580d2dc5e03eb..9a8d4843bf6a43 100644 --- a/Mathlib/Order/Sublattice.lean +++ b/Mathlib/Order/Sublattice.lean @@ -396,4 +396,16 @@ lemma pi_univ_eq_bot {L : ∀ i, Sublattice (π i)} {i : κ} (hL : L i = ⊥) : pi_univ_eq_bot_iff.2 ⟨i, hL⟩ end Pi + +namespace LatticeHom + +/-- +The image of `LatticeHom` is a sublattice. +-/ +def range (f : LatticeHom α β) := (Sublattice.map f ⊤).copy (Set.range f) image_univ.symm + +lemma range_coe : (LatticeHom.range f : Set β) = Set.range f := rfl + +end LatticeHom + end Sublattice From 87ebddae7d1f5bbbd86387a98dd0d138a14afd93 Mon Sep 17 00:00:00 2001 From: Bergschaf Date: Wed, 29 Apr 2026 23:11:41 +0200 Subject: [PATCH 2/2] comment --- Mathlib/Order/Sublattice.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Order/Sublattice.lean b/Mathlib/Order/Sublattice.lean index 9a8d4843bf6a43..1bd5cbc2b04b76 100644 --- a/Mathlib/Order/Sublattice.lean +++ b/Mathlib/Order/Sublattice.lean @@ -400,7 +400,7 @@ end Pi namespace LatticeHom /-- -The image of `LatticeHom` is a sublattice. +The range of `LatticeHom` is a sublattice. -/ def range (f : LatticeHom α β) := (Sublattice.map f ⊤).copy (Set.range f) image_univ.symm