BanLat/Substructures/Sublattice.lean
All source files · Download exact source
SHA-256: e2df596909a94e153be31e04957c4e218d2d763ceeb97a3fec016e18de8c3ea6
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Disjoint6import BanLat.LLexpr7import BanLat.Normed8import Mathlib.Algebra.Group.Pointwise.Set.Basic9import Mathlib.Geometry.Convex.Cone.Pointed10import Mathlib.Order.Sublattice11import Mathlib.Order.SupClosed1213/-!14# Sublattices of vector lattices1516A **vector sublattice** of a vector lattice is a linear subspace closed under the lattice17operations. Since all lattice operations are expressible in terms of each other, it suffices18that the subspace be closed under any one operation — for example, `⊔` or `|·|`. The key19characterisation proved here is that closure under absolute value is equivalent to the20sublattice property. The file also constructs generated sublattices, describes21them in terms of sup- and inf-closures, and records the induced normed vector22lattice structure on closed sublattices.23-/2425variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]26 [VectorLattice X]2728/-! ### Sup- and inf-closure of a pointed cone2930In a vector lattice, the sup-closure and inf-closure of a pointed cone31`C ⊆ X` are again pointed cones. -/3233namespace PointedCone3435omit [VectorLattice X] in36/-- If `s` is closed under addition, so is its sup-closure. -/37private theorem add_mem_supClosure_of_addClosed {s : Set X}38 (hadd : ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a + b ∈ s)39 {x y : X} (hx : x ∈ _root_.supClosure s) (hy : y ∈ _root_.supClosure s) :40 x + y ∈ _root_.supClosure s := by41 have step : ∀ a ∈ s, ∀ b ∈ _root_.supClosure s, a + b ∈ _root_.supClosure s := by42 intro a ha b hb43 have h_sc : SupClosed {c : X | a + c ∈ _root_.supClosure s} := fun u hu v hv => by44 change a + (u ⊔ v) ∈ _root_.supClosure s45 rw [add_sup]; exact supClosed_supClosure hu hv46 have hsub : s ⊆ {c : X | a + c ∈ _root_.supClosure s} :=47 fun c hc => subset_supClosure (hadd ha hc)48 exact supClosure_min hsub h_sc hb49 have h_sc : SupClosed {c : X | c + y ∈ _root_.supClosure s} := fun u hu v hv => by50 change (u ⊔ v) + y ∈ _root_.supClosure s51 rw [sup_add]; exact supClosed_supClosure hu hv52 have hsub : s ⊆ {c : X | c + y ∈ _root_.supClosure s} :=53 fun c hc => step c hc y hy54 exact supClosure_min hsub h_sc hx5556/-- If `s` is closed under non-negative scaling, so is its sup-closure. -/57private theorem smul_mem_supClosure_of_smulClosed {s : Set X}58 (hsmul : ∀ ⦃a : ℝ⦄, 0 ≤ a → ∀ ⦃x⦄, x ∈ s → a • x ∈ s)59 {a : ℝ} (ha : 0 ≤ a) {x : X} (hx : x ∈ _root_.supClosure s) :60 a • x ∈ _root_.supClosure s := by61 have h_sc : SupClosed {c : X | a • c ∈ _root_.supClosure s} := fun u hu v hv => by62 change a • (u ⊔ v) ∈ _root_.supClosure s63 rw [nonneg_smul_sup u v a ha]; exact supClosed_supClosure hu hv64 have hsub : s ⊆ {c : X | a • c ∈ _root_.supClosure s} :=65 fun c hc => subset_supClosure (hsmul ha hc)66 exact supClosure_min hsub h_sc hx6768omit [VectorLattice X] in69/-- If `s` is closed under addition, so is its inf-closure. -/70private theorem add_mem_infClosure_of_addClosed {s : Set X}71 (hadd : ∀ ⦃a⦄, a ∈ s → ∀ ⦃b⦄, b ∈ s → a + b ∈ s)72 {x y : X} (hx : x ∈ _root_.infClosure s) (hy : y ∈ _root_.infClosure s) :73 x + y ∈ _root_.infClosure s := by74 have step : ∀ a ∈ s, ∀ b ∈ _root_.infClosure s, a + b ∈ _root_.infClosure s := by75 intro a ha b hb76 have h_ic : InfClosed {c : X | a + c ∈ _root_.infClosure s} := fun u hu v hv => by77 change a + (u ⊓ v) ∈ _root_.infClosure s78 rw [add_inf]; exact infClosed_infClosure hu hv79 have hsub : s ⊆ {c : X | a + c ∈ _root_.infClosure s} :=80 fun c hc => subset_infClosure (hadd ha hc)81 exact infClosure_min hsub h_ic hb82 have h_ic : InfClosed {c : X | c + y ∈ _root_.infClosure s} := fun u hu v hv => by83 change (u ⊓ v) + y ∈ _root_.infClosure s84 rw [inf_add]; exact infClosed_infClosure hu hv85 have hsub : s ⊆ {c : X | c + y ∈ _root_.infClosure s} :=86 fun c hc => step c hc y hy87 exact infClosure_min hsub h_ic hx8889/-- If `s` is closed under non-negative scaling, so is its inf-closure. -/90private theorem smul_mem_infClosure_of_smulClosed {s : Set X}91 (hsmul : ∀ ⦃a : ℝ⦄, 0 ≤ a → ∀ ⦃x⦄, x ∈ s → a • x ∈ s)92 {a : ℝ} (ha : 0 ≤ a) {x : X} (hx : x ∈ _root_.infClosure s) :93 a • x ∈ _root_.infClosure s := by94 have h_ic : InfClosed {c : X | a • c ∈ _root_.infClosure s} := fun u hu v hv => by95 change a • (u ⊓ v) ∈ _root_.infClosure s96 rw [nonneg_smul_inf u v a ha]; exact infClosed_infClosure hu hv97 have hsub : s ⊆ {c : X | a • c ∈ _root_.infClosure s} :=98 fun c hc => subset_infClosure (hsmul ha hc)99 exact infClosure_min hsub h_ic hx100101/-- The sup-closure of a pointed cone is a pointed cone. -/102def supClosure (C : PointedCone ℝ X) : PointedCone ℝ X where103 carrier := _root_.supClosure (C : Set X)104 zero_mem' := subset_supClosure C.zero_mem105 add_mem' hx hy := add_mem_supClosure_of_addClosed (fun _ hx _ hy => C.add_mem hx hy) hx hy106 smul_mem' c _ hx :=107 smul_mem_supClosure_of_smulClosed (fun _ ha _ hx => C.smul_mem ha hx) c.2 hx108109@[simp]110theorem coe_supClosure (C : PointedCone ℝ X) :111 (supClosure C : Set X) = _root_.supClosure (C : Set X) := rfl112113/-- The inf-closure of a pointed cone is a pointed cone. -/114def infClosure (C : PointedCone ℝ X) : PointedCone ℝ X where115 carrier := _root_.infClosure (C : Set X)116 zero_mem' := subset_infClosure C.zero_mem117 add_mem' hx hy := add_mem_infClosure_of_addClosed (fun _ hx _ hy => C.add_mem hx hy) hx hy118 smul_mem' c _ hx :=119 smul_mem_infClosure_of_smulClosed (fun _ ha _ hx => C.smul_mem ha hx) c.2 hx120121@[simp]122theorem coe_infClosure (C : PointedCone ℝ X) :123 (infClosure C : Set X) = _root_.infClosure (C : Set X) := rfl124125end PointedCone126127/-- A `VectorSublattice` of a vector lattice `X` is a linear subspace closed under128`⊔`. This is the bundled version: it extends `Submodule ℝ X` with lattice closure. -/129structure VectorSublattice (X : Type*) [AddCommGroup X] [Lattice X]130 [IsOrderedAddMonoid X] [VectorLattice X] extends Submodule ℝ X where131 sup_mem' : ∀ {x y : X}, x ∈ carrier → y ∈ carrier → x ⊔ y ∈ carrier132133namespace VectorSublattice134135instance : SetLike (VectorSublattice X) X where136 coe Y := Y.carrier137 coe_injective p q h := by138 cases p; cases q; congr139 exact SetLike.ext' h140141variable (Y : VectorSublattice X)142143/-- A vector sublattice is closed under `⊔`. -/144theorem sup_mem {x y : X} (hx : x ∈ Y) (hy : y ∈ Y) :145 x ⊔ y ∈ Y :=146 Y.sup_mem' hx hy147148/-- A vector sublattice is closed under `⊓`. -/149theorem inf_mem {x y : X} (hx : x ∈ Y) (hy : y ∈ Y) :150 x ⊓ y ∈ Y := by151 rw [inf_eq_sub_posPart x y]152 exact Y.toSubmodule.sub_mem hx (Y.sup_mem' (Y.toSubmodule.sub_mem hx hy) (Y.toSubmodule.zero_mem))153154/-- A vector sublattice is closed under the positive part. -/155theorem posPart_mem {x : X} (hx : x ∈ Y) : x⁺ ∈ Y :=156 Y.sup_mem' hx (Y.toSubmodule.zero_mem)157158/-- A vector sublattice is closed under the negative part. -/159theorem negPart_mem {x : X} (hx : x ∈ Y) : x⁻ ∈ Y :=160 posPart_mem Y (Y.toSubmodule.neg_mem hx)161162/-- A vector sublattice is closed under absolute value. -/163theorem abs_mem {x : X} (hx : x ∈ Y) : |x| ∈ Y :=164 sup_mem Y hx (Y.toSubmodule.neg_mem hx)165166/-- The underlying set of a vector sublattice is an `IsSublattice`. -/167theorem isSublattice : IsSublattice (Y : Set X) where168 supClosed := by intro _ ha _ hb; exact sup_mem Y ha hb169 infClosed := by intro _ ha _ hb; exact inf_mem Y ha hb170171/-! ### Construction from absolute-value closure -/172173/-- The positive part lies in a submodule closed under absolute value. -/174private theorem posPart_mem_of_absClosed (M : Submodule ℝ X)175 (h : ∀ x : X, x ∈ M → |x| ∈ M) {x : X} (hx : x ∈ M) : x⁺ ∈ M := by176 have key : x + |x| = 2 • x⁺ := add_abs_eq_two_nsmul_posPart x177 have h2 : (2 : ℝ)⁻¹ • (x + |x|) = x⁺ := by178 rw [key, ← Nat.cast_smul_eq_nsmul ℝ 2]; norm_num [smul_smul]179 rw [← h2]180 exact M.smul_mem _ (M.add_mem hx (h x hx))181182/-- Build a `VectorSublattice` from a submodule closed under `|·|`. -/183def ofAbsClosed (M : Submodule ℝ X)184 (h : ∀ x : X, x ∈ M → |x| ∈ M) : VectorSublattice X where185 toSubmodule := M186 sup_mem' := fun {x y} hx hy => by187 rw [sup_eq_add_posPart x y]188 exact M.add_mem hx (posPart_mem_of_absClosed M h (M.sub_mem hy hx))189190/-- A submodule is a vector sublattice iff it is closed under absolute value. -/191theorem abs_mem_iff_sup_mem (M : Submodule ℝ X) :192 (∀ x : X, x ∈ M → |x| ∈ M) ↔193 ∀ x y : X, x ∈ M → y ∈ M → x ⊔ y ∈ M := by194 constructor195 · intro h x y hx hy196 exact (ofAbsClosed M h).sup_mem' hx hy197 · intro h x hx198 exact h x (-x) hx (M.neg_mem hx)199200/-! ### Coercion to submodule -/201202/-- The coercion to `Submodule ℝ X` is injective. -/203theorem toSubmodule_injective :204 Function.Injective205 (toSubmodule : VectorSublattice X → Submodule ℝ X) := by206 intro p q h207 cases p; cases q; congr208209/-- A vector sublattice and its underlying submodule have the same carrier. -/210@[simp]211theorem coe_toSubmodule : (Y.toSubmodule : Set X) = (Y : Set X) := rfl212213/-! ### Coercion to pointed cone214215Every vector sublattice, being a linear subspace, is in particular a pointed216convex cone. -/217218/-- Every vector sublattice is (canonically) a pointed cone. -/219instance : CoeHead (VectorSublattice X) (PointedCone ℝ X) where220 coe Y :=221 { toAddSubmonoid := Y.toSubmodule.toAddSubmonoid222 smul_mem' := fun c _ hx => Y.toSubmodule.smul_mem c.1 hx }223224theorem coe_toPointedCone (Y : VectorSublattice X) :225 ((Y : PointedCone ℝ X) : Set X) = (Y : Set X) := rfl226227/-! ### Lattice structure on the underlying subtype228229A vector sublattice `Y` inherits a lattice and vector-lattice structure from230the ambient space, with `⊔` and `⊓` computed pointwise. -/231232/-- The lattice structure on the underlying subtype of a vector sublattice. -/233noncomputable instance instLatticeSubtype : Lattice ↥Y.toSubmodule :=234 Subtype.lattice (P := fun x => x ∈ Y.toSubmodule)235 (fun _ _ hx hy => Y.sup_mem hx hy) (fun _ _ hx hy => Y.inf_mem hx hy)236237/-- The subtype of a vector sublattice is an ordered additive monoid. -/238instance instIsOrderedAddMonoidSubtype :239 IsOrderedAddMonoid ↥Y.toSubmodule where240 add_le_add_left := by241 intro a b (h : a.1 ≤ b.1) c; exact add_le_add_left h c.1242 add_le_add_right := by243 intro a b (h : a.1 ≤ b.1) c; exact add_le_add_right h c.1244245/-- Scalar multiplication by non-negative reals is monotone on the subtype of246a vector sublattice. -/247instance instPosSMulMonoSubtype : PosSMulMono ℝ ↥Y.toSubmodule where248 smul_le_smul_of_nonneg_left := by249 intro a ha b₁ b₂ h250 change (a • b₁).1 ≤ (a • b₂).1251 exact smul_le_smul_of_nonneg_left h ha252253/-- The subtype of a vector sublattice is itself a vector lattice. -/254instance instVectorLatticeSubtype : VectorLattice ↥Y.toSubmodule := ⟨⟩255256/-! ### Lattice structure on `VectorSublattice X`257258The collection of vector sublattices of `X` is ordered by inclusion. It259contains the whole space `⊤ = X` and the zero subspace `⊥ = {0}`, and is260closed under arbitrary intersections. -/261262instance : PartialOrder (VectorSublattice X) :=263 PartialOrder.lift (fun Y => (Y : Set X)) SetLike.coe_injective264265/-- The whole space `X` is a vector sublattice. -/266instance : Top (VectorSublattice X) where267 top :=268 { toSubmodule := ⊤269 sup_mem' := fun _ _ => Submodule.mem_top }270271/-- Every element belongs to `⊤`. -/272@[simp]273theorem mem_top {x : X} : x ∈ (⊤ : VectorSublattice X) :=274 Submodule.mem_top275276/-- The zero subspace `{0}` is a vector sublattice. -/277instance : Bot (VectorSublattice X) where278 bot :=279 { toSubmodule := ⊥280 sup_mem' := fun {x y} hx hy => by281 have hx' : x = 0 := (Submodule.mem_bot ℝ).mp hx282 have hy' : y = 0 := (Submodule.mem_bot ℝ).mp hy283 rw [hx', hy', sup_idem]; exact Submodule.zero_mem _ }284285/-- An element of `⊥` is zero. -/286@[simp]287theorem mem_bot {x : X} : x ∈ (⊥ : VectorSublattice X) ↔ x = 0 :=288 Submodule.mem_bot ℝ289290/-- Arbitrary intersections of vector sublattices are vector sublattices. -/291instance : InfSet (VectorSublattice X) where292 sInf S :=293 { toSubmodule := sInf ((·.toSubmodule) '' S)294 sup_mem' := fun {x y} hx hy => by295 have hx' := (Submodule.mem_sInf).mp hx296 have hy' := (Submodule.mem_sInf).mp hy297 refine (Submodule.mem_sInf).mpr ?_298 rintro _ ⟨Y, hY, rfl⟩299 exact Y.sup_mem (hx' _ ⟨Y, hY, rfl⟩) (hy' _ ⟨Y, hY, rfl⟩) }300301/-! ### The vector sublattice generated by a set302303The vector sublattice generated by a set `s ⊆ X` is by definition the304smallest vector sublattice of `X` containing `s`, obtained as the infimum305of all vector sublattices containing `s`. -/306307/-- The vector sublattice generated by a set `s`: the smallest vector308sublattice of `X` containing `s`. -/309def generated (s : Set X) : VectorSublattice X :=310 sInf {Y : VectorSublattice X | s ⊆ Y}311312/-- The generating set is contained in the vector sublattice it generates. -/313theorem subset_generated (s : Set X) : s ⊆ (generated s : Set X) := by314 intro x hx315 refine (Submodule.mem_sInf).mpr ?_316 rintro _ ⟨Y, hY, rfl⟩317 exact hY hx318319/-- The vector sublattice generated by `s` is contained in every vector320sublattice containing `s`. -/321theorem generated_le {s : Set X} {Y : VectorSublattice X} (h : s ⊆ Y) :322 generated s ≤ Y := by323 intro x hx324 have := (Submodule.mem_sInf).mp hx325 exact this _ ⟨Y, h, rfl⟩326327/-- For a submodule `M`, its lattice closure is closed under addition. -/328private lemma latticeClosure_add_mem_of_submodule (M : Submodule ℝ X)329 {x y : X} (hx : x ∈ latticeClosure (M : Set X))330 (hy : y ∈ latticeClosure (M : Set X)) :331 x + y ∈ latticeClosure (M : Set X) := by332 letI := AddCommGroup.toDistribLattice X333 refine latticeClosure_sup_inf_induction334 (p := fun a _ => a + y ∈ latticeClosure (M : Set X)) ?_ ?_ ?_ hx335 · intro a ha336 refine latticeClosure_sup_inf_induction337 (p := fun b _ => a + b ∈ latticeClosure (M : Set X)) ?_ ?_ ?_ hy338 · intro b hb; exact subset_latticeClosure (M.add_mem ha hb)339 · intro p _ q _ h₁ h₂340 rw [add_sup]; exact isSublattice_latticeClosure.supClosed h₁ h₂341 · intro p _ q _ h₁ h₂342 rw [add_inf]; exact isSublattice_latticeClosure.infClosed h₁ h₂343 · intro p _ q _ h₁ h₂344 rw [sup_add]; exact isSublattice_latticeClosure.supClosed h₁ h₂345 · intro p _ q _ h₁ h₂346 rw [inf_add]; exact isSublattice_latticeClosure.infClosed h₁ h₂347348/-- For a submodule `M`, its lattice closure is closed under scaling. -/349private lemma latticeClosure_smul_mem_of_submodule (M : Submodule ℝ X)350 (c : ℝ) {x : X} (hx : x ∈ latticeClosure (M : Set X)) :351 c • x ∈ latticeClosure (M : Set X) := by352 letI := AddCommGroup.toDistribLattice X353 rcases le_or_gt 0 c with hc | hc354 · refine latticeClosure_sup_inf_induction355 (p := fun a _ => c • a ∈ latticeClosure (M : Set X)) ?_ ?_ ?_ hx356 · intro a ha; exact subset_latticeClosure (M.smul_mem c ha)357 · intro p _ q _ h₁ h₂358 rw [nonneg_smul_sup p q c hc]359 exact isSublattice_latticeClosure.supClosed h₁ h₂360 · intro p _ q _ h₁ h₂361 rw [nonneg_smul_inf p q c hc]362 exact isSublattice_latticeClosure.infClosed h₁ h₂363 · have hc' : 0 ≤ -c := by linarith364 refine latticeClosure_sup_inf_induction365 (p := fun a _ => c • a ∈ latticeClosure (M : Set X)) ?_ ?_ ?_ hx366 · intro a ha; exact subset_latticeClosure (M.smul_mem c ha)367 · intro p _ q _ h₁ h₂368 have eq : c • (p ⊔ q) = (c • p) ⊓ (c • q) := by369 rw [show c • (p ⊔ q) = -((-c) • (p ⊔ q)) by rw [neg_smul, neg_neg],370 nonneg_smul_sup p q (-c) hc', neg_sup, neg_smul, neg_neg, neg_smul, neg_neg]371 rw [eq]372 exact isSublattice_latticeClosure.infClosed h₁ h₂373 · intro p _ q _ h₁ h₂374 have eq : c • (p ⊓ q) = (c • p) ⊔ (c • q) := by375 rw [show c • (p ⊓ q) = -((-c) • (p ⊓ q)) by rw [neg_smul, neg_neg],376 nonneg_smul_inf p q (-c) hc', neg_inf, neg_smul, neg_neg, neg_smul, neg_neg]377 rw [eq]378 exact isSublattice_latticeClosure.supClosed h₁ h₂379380/-- The vector sublattice whose underlying set is the lattice closure of a381submodule. -/382private def sublatticeOfSubmoduleLatticeClosure (M : Submodule ℝ X) :383 VectorSublattice X where384 toSubmodule :=385 { carrier := latticeClosure (M : Set X)386 zero_mem' := subset_latticeClosure M.zero_mem387 add_mem' := latticeClosure_add_mem_of_submodule M388 smul_mem' := latticeClosure_smul_mem_of_submodule M }389 sup_mem' := fun {_ _} hx hy => by390 letI := AddCommGroup.toDistribLattice X391 exact isSublattice_latticeClosure.supClosed hx hy392393/-- The vector sublattice generated by a linear subspace `M` coincides with394the sup-closure of the inf-closure of `M`. -/395theorem generated_submodule_eq_supClosure_infClosure (M : Submodule ℝ X) :396 (generated (M : Set X) : Set X) = supClosure (infClosure (M : Set X)) := by397 letI := AddCommGroup.toDistribLattice X398 rw [supClosure_infClosure]399 refine Set.Subset.antisymm ?_ ?_400 · have h : (M : Set X) ⊆ (sublatticeOfSubmoduleLatticeClosure M : Set X) :=401 fun _ hx => subset_latticeClosure hx402 exact generated_le h403 · exact latticeClosure_min (subset_generated _)404 (generated (M : Set X)).isSublattice405406/-- The vector sublattice generated by a linear subspace `M` coincides with407the inf-closure of the sup-closure of `M`. -/408theorem generated_submodule_eq_infClosure_supClosure (M : Submodule ℝ X) :409 (generated (M : Set X) : Set X) = infClosure (supClosure (M : Set X)) := by410 letI := AddCommGroup.toDistribLattice X411 rw [infClosure_supClosure, ← supClosure_infClosure]412 exact generated_submodule_eq_supClosure_infClosure M413414open scoped Pointwise in415/-- The difference set `supClosure C - supClosure C` of a pointed cone is a416vector sublattice. -/417private def sublatticeOfConeSupClosureDiff (C : PointedCone ℝ X) :418 VectorSublattice X where419 toSubmodule :=420 { carrier := _root_.supClosure (C : Set X) - _root_.supClosure (C : Set X)421 zero_mem' :=422 ⟨0, subset_supClosure C.zero_mem, 0, subset_supClosure C.zero_mem, sub_self 0⟩423 add_mem' := by424 rintro _ _ ⟨u₁, hu₁, v₁, hv₁, rfl⟩ ⟨u₂, hu₂, v₂, hv₂, rfl⟩425 refine ⟨u₁ + u₂, ?_, v₁ + v₂, ?_, ?_⟩426 · exact PointedCone.add_mem_supClosure_of_addClosed427 (fun _ h _ h' => C.add_mem h h') hu₁ hu₂428 · exact PointedCone.add_mem_supClosure_of_addClosed429 (fun _ h _ h' => C.add_mem h h') hv₁ hv₂430 · change (u₁ + u₂) - (v₁ + v₂) = (u₁ - v₁) + (u₂ - v₂); abel431 smul_mem' := by432 rintro c _ ⟨u, hu, v, hv, rfl⟩433 rcases le_or_gt 0 c with hc | hc434 · refine ⟨c • u, ?_, c • v, ?_, ?_⟩435 · exact PointedCone.smul_mem_supClosure_of_smulClosed436 (fun _ h _ h' => C.smul_mem h h') hc hu437 · exact PointedCone.smul_mem_supClosure_of_smulClosed438 (fun _ h _ h' => C.smul_mem h h') hc hv439 · change c • u - c • v = c • (u - v); rw [smul_sub]440 · have hc' : 0 ≤ -c := by linarith441 refine ⟨(-c) • v, ?_, (-c) • u, ?_, ?_⟩442 · exact PointedCone.smul_mem_supClosure_of_smulClosed443 (fun _ h _ h' => C.smul_mem h h') hc' hv444 · exact PointedCone.smul_mem_supClosure_of_smulClosed445 (fun _ h _ h' => C.smul_mem h h') hc' hu446 · change (-c) • v - (-c) • u = c • (u - v)447 rw [smul_sub, neg_smul, neg_smul]; abel }448 sup_mem' := by449 rintro _ _ ⟨u₁, hu₁, v₁, hv₁, rfl⟩ ⟨u₂, hu₂, v₂, hv₂, rfl⟩450 refine ⟨(u₁ + v₂) ⊔ (u₂ + v₁), ?_, v₁ + v₂, ?_, ?_⟩451 · exact supClosed_supClosure452 (PointedCone.add_mem_supClosure_of_addClosed453 (fun _ h _ h' => C.add_mem h h') hu₁ hv₂)454 (PointedCone.add_mem_supClosure_of_addClosed455 (fun _ h _ h' => C.add_mem h h') hu₂ hv₁)456 · exact PointedCone.add_mem_supClosure_of_addClosed457 (fun _ h _ h' => C.add_mem h h') hv₁ hv₂458 · have h : ((u₁ - v₁) ⊔ (u₂ - v₂)) + (v₁ + v₂) = (u₁ + v₂) ⊔ (u₂ + v₁) := by459 rw [sup_add]; congr 1 <;> abel460 change ((u₁ + v₂) ⊔ (u₂ + v₁)) - (v₁ + v₂) = (u₁ - v₁) ⊔ (u₂ - v₂)461 rw [← h]; abel462463open scoped Pointwise in464/-- The vector sublattice generated by a pointed cone `C` coincides with the465difference set of the sup-closure of `C` with itself. -/466theorem generated_pointedCone_eq_sub_supClosure (C : PointedCone ℝ X) :467 (generated (C : Set X) : Set X)468 = supClosure (C : Set X) - supClosure (C : Set X) := by469 refine Set.Subset.antisymm ?_ ?_470 · have h : (C : Set X) ⊆ (sublatticeOfConeSupClosureDiff C : Set X) := fun x hx =>471 ⟨x, subset_supClosure hx, 0, subset_supClosure C.zero_mem, sub_zero x⟩472 exact generated_le h473 · rintro _ ⟨u, hu, v, hv, rfl⟩474 have hC : (C : Set X) ⊆ (generated (C : Set X) : Set X) := subset_generated _475 have h_sup : SupClosed (generated (C : Set X) : Set X) :=476 (generated (C : Set X)).isSublattice.supClosed477 have hu_gen := supClosure_min hC h_sup hu478 have hv_gen := supClosure_min hC h_sup hv479 exact (generated (C : Set X)).toSubmodule.sub_mem hu_gen hv_gen480481open scoped Pointwise in482/-- The difference set `infClosure C - infClosure C` of a pointed cone is a483vector sublattice. -/484private def sublatticeOfConeInfClosureDiff (C : PointedCone ℝ X) :485 VectorSublattice X where486 toSubmodule :=487 { carrier := _root_.infClosure (C : Set X) - _root_.infClosure (C : Set X)488 zero_mem' :=489 ⟨0, subset_infClosure C.zero_mem, 0, subset_infClosure C.zero_mem, sub_self 0⟩490 add_mem' := by491 rintro _ _ ⟨u₁, hu₁, v₁, hv₁, rfl⟩ ⟨u₂, hu₂, v₂, hv₂, rfl⟩492 refine ⟨u₁ + u₂, ?_, v₁ + v₂, ?_, ?_⟩493 · exact PointedCone.add_mem_infClosure_of_addClosed494 (fun _ h _ h' => C.add_mem h h') hu₁ hu₂495 · exact PointedCone.add_mem_infClosure_of_addClosed496 (fun _ h _ h' => C.add_mem h h') hv₁ hv₂497 · change (u₁ + u₂) - (v₁ + v₂) = (u₁ - v₁) + (u₂ - v₂); abel498 smul_mem' := by499 rintro c _ ⟨u, hu, v, hv, rfl⟩500 rcases le_or_gt 0 c with hc | hc501 · refine ⟨c • u, ?_, c • v, ?_, ?_⟩502 · exact PointedCone.smul_mem_infClosure_of_smulClosed503 (fun _ h _ h' => C.smul_mem h h') hc hu504 · exact PointedCone.smul_mem_infClosure_of_smulClosed505 (fun _ h _ h' => C.smul_mem h h') hc hv506 · change c • u - c • v = c • (u - v); rw [smul_sub]507 · have hc' : 0 ≤ -c := by linarith508 refine ⟨(-c) • v, ?_, (-c) • u, ?_, ?_⟩509 · exact PointedCone.smul_mem_infClosure_of_smulClosed510 (fun _ h _ h' => C.smul_mem h h') hc' hv511 · exact PointedCone.smul_mem_infClosure_of_smulClosed512 (fun _ h _ h' => C.smul_mem h h') hc' hu513 · change (-c) • v - (-c) • u = c • (u - v)514 rw [smul_sub, neg_smul, neg_smul]; abel }515 sup_mem' := by516 rintro _ _ ⟨u₁, hu₁, v₁, hv₁, rfl⟩ ⟨u₂, hu₂, v₂, hv₂, rfl⟩517 have hadd : ∀ ⦃a⦄, a ∈ (C : Set X) → ∀ ⦃b⦄, b ∈ (C : Set X) → a + b ∈ (C : Set X) :=518 fun _ ha _ hb => C.add_mem ha hb519 have hu₁v₂ : u₁ + v₂ ∈ _root_.infClosure (C : Set X) :=520 PointedCone.add_mem_infClosure_of_addClosed hadd hu₁ hv₂521 have hu₂v₁ : u₂ + v₁ ∈ _root_.infClosure (C : Set X) :=522 PointedCone.add_mem_infClosure_of_addClosed hadd hu₂ hv₁523 have hv₁v₂ : v₁ + v₂ ∈ _root_.infClosure (C : Set X) :=524 PointedCone.add_mem_infClosure_of_addClosed hadd hv₁ hv₂525 have hinf : (u₁ + v₂) ⊓ (u₂ + v₁) ∈ _root_.infClosure (C : Set X) :=526 infClosed_infClosure hu₁v₂ hu₂v₁527 refine ⟨u₁ + u₂ + v₁ + v₂, ?_, (u₁ + v₂) ⊓ (u₂ + v₁) + (v₁ + v₂), ?_, ?_⟩528 · have heq : u₁ + u₂ + v₁ + v₂ = (u₁ + v₂) + (u₂ + v₁) := by abel529 rw [heq]530 exact PointedCone.add_mem_infClosure_of_addClosed hadd hu₁v₂ hu₂v₁531 · exact PointedCone.add_mem_infClosure_of_addClosed hadd hinf hv₁v₂532 · have step1 : (u₁ + v₂) ⊔ (u₂ + v₁) =533 (u₁ + v₂) + (u₂ + v₁) - (u₁ + v₂) ⊓ (u₂ + v₁) := by534 rw [eq_sub_iff_add_eq, add_comm]535 exact inf_add_sup _ _536 have step2 : ((u₁ - v₁) ⊔ (u₂ - v₂)) + (v₁ + v₂) =537 (u₁ + v₂) ⊔ (u₂ + v₁) := by538 rw [sup_add]; congr 1 <;> abel539 change u₁ + u₂ + v₁ + v₂ - ((u₁ + v₂) ⊓ (u₂ + v₁) + (v₁ + v₂))540 = (u₁ - v₁) ⊔ (u₂ - v₂)541 symm542 calc (u₁ - v₁) ⊔ (u₂ - v₂)543 = ((u₁ + v₂) ⊔ (u₂ + v₁)) - (v₁ + v₂) := by rw [← step2]; abel544 _ = ((u₁ + v₂) + (u₂ + v₁) - (u₁ + v₂) ⊓ (u₂ + v₁)) - (v₁ + v₂) := by rw [← step1]545 _ = u₁ + u₂ + v₁ + v₂ - ((u₁ + v₂) ⊓ (u₂ + v₁) + (v₁ + v₂)) := by abel546547open scoped Pointwise in548/-- The vector sublattice generated by a pointed cone `C` coincides with the549difference set of the inf-closure of `C` with itself. -/550theorem generated_pointedCone_eq_sub_infClosure (C : PointedCone ℝ X) :551 (generated (C : Set X) : Set X)552 = infClosure (C : Set X) - infClosure (C : Set X) := by553 refine Set.Subset.antisymm ?_ ?_554 · have h : (C : Set X) ⊆ (sublatticeOfConeInfClosureDiff C : Set X) := fun x hx =>555 ⟨x, subset_infClosure hx, 0, subset_infClosure C.zero_mem, sub_zero x⟩556 exact generated_le h557 · rintro _ ⟨u, hu, v, hv, rfl⟩558 have hC : (C : Set X) ⊆ (generated (C : Set X) : Set X) := subset_generated _559 have h_inf : InfClosed (generated (C : Set X) : Set X) :=560 (generated (C : Set X)).isSublattice.infClosed561 have hu_gen := infClosure_min hC h_inf hu562 have hv_gen := infClosure_min hC h_inf hv563 exact (generated (C : Set X)).toSubmodule.sub_mem hu_gen hv_gen564565omit [VectorLattice X] in566/-- For a finite set `s` of pairwise lattice-disjoint elements and a family567`g : X → X` taking values disjoint from a fixed `a`, the sum over `s` remains568lattice-disjoint from `a`. -/569private lemma isVLDisjoint_finsetSum {a : X} {s : Finset X} {g : X → X}570 (h : ∀ i ∈ s, IsVLDisjoint a (g i)) :571 IsVLDisjoint a (∑ i ∈ s, g i) := by572 classical573 induction s using Finset.induction_on with574 | empty => simpa using isVLDisjoint_zero_right a575 | insert b s hb ih =>576 rw [Finset.sum_insert hb]577 refine (h b (Finset.mem_insert_self b s)).add_right ?_578 exact ih (fun i hi => h i (Finset.mem_insert_of_mem hi))579580/-- Disjoint sum of a scalar family: for a Finset `s` of pairwise-disjoint581elements with any scalars `f`, `|∑ f(a) • a| = ∑ |f(a)| • |a|`. -/582private lemma abs_sum_finset_of_pairwise_vlDisjoint {s : Finset X} {f : X → ℝ}583 (hdisj : (s : Set X).Pairwise IsVLDisjoint) :584 |∑ a ∈ s, f a • a| = ∑ a ∈ s, |f a| • |a| := by585 classical586 induction s using Finset.induction_on with587 | empty => simp588 | insert a s ha ih =>589 have hdisj_s : (s : Set X).Pairwise IsVLDisjoint := fun i hi j hj hij =>590 hdisj (Finset.mem_insert_of_mem hi) (Finset.mem_insert_of_mem hj) hij591 rw [Finset.sum_insert ha, Finset.sum_insert ha]592 have hdisj_head : IsVLDisjoint (f a • a) (∑ i ∈ s, f i • i) := by593 apply isVLDisjoint_finsetSum594 intro i hi595 have hne_ai : a ≠ i := fun h => ha (h ▸ hi)596 exact ((hdisj (Finset.mem_insert_self a s)597 (Finset.mem_insert_of_mem hi) hne_ai).smul_left (f a)).smul_right (f i)598 rw [abs_add_of_isVLDisjoint hdisj_head, abs_smul', ih hdisj_s]599600/-- The vector sublattice generated by a set of pairwise lattice-disjoint,601non-negative elements coincides with its linear span. -/602theorem generated_eq_span_of_pairwise_vlDisjoint {A : Set X}603 (hA : A.Pairwise IsVLDisjoint) (hA_nn : ∀ a ∈ A, 0 ≤ a) :604 (generated A).toSubmodule = Submodule.span ℝ A := by605 refine le_antisymm ?_ (Submodule.span_le.mpr (subset_generated A))606 have h_abs : ∀ u, u ∈ Submodule.span ℝ A → |u| ∈ Submodule.span ℝ A := by607 intro u hu608 obtain ⟨f, t, ht_sub, _, hsum⟩ :=609 Submodule.mem_span_iff_exists_finset_subset.mp hu610 have hdisj_t : (t : Set X).Pairwise IsVLDisjoint := fun i hi j hj hij =>611 hA (ht_sub hi) (ht_sub hj) hij612 have hnn_t : ∀ a ∈ t, 0 ≤ a := fun a ha => hA_nn a (ht_sub ha)613 rw [← hsum, abs_sum_finset_of_pairwise_vlDisjoint hdisj_t]614 refine Submodule.sum_mem _ fun a ha => ?_615 rw [abs_of_nonneg (hnn_t a ha)]616 exact Submodule.smul_mem _ _ (Submodule.subset_span (ht_sub ha))617 let Y : VectorSublattice X := ofAbsClosed (Submodule.span ℝ A) h_abs618 have hA_sub : A ⊆ (Y : Set X) := Submodule.subset_span619 have hle := generated_le (Y := Y) hA_sub620 intro x hx621 exact hle hx622623end VectorSublattice624625namespace LLexpr626627variable {n : ℕ}628629section Combinations630631variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]632 [VectorLattice X]633634/-- The sublattice generated by the image of a tuple `x : Fin n → X` coincides635with the set of lattice-linear combinations of `x`. -/636theorem generated_range_eq_combinations (x : Fin n → X) :637 (VectorSublattice.generated (Set.range x) : Set X)638 = combinations x := by639 let Y : VectorSublattice X :=640 { toSubmodule :=641 { carrier := combinations x642 zero_mem' := ⟨.zero, rfl⟩643 add_mem' := by644 rintro _ _ ⟨e₁, rfl⟩ ⟨e₂, rfl⟩645 exact ⟨.add e₁ e₂, rfl⟩646 smul_mem' := by647 rintro r _ ⟨e, rfl⟩648 exact ⟨.smul r e, rfl⟩ }649 sup_mem' := by650 rintro _ _ ⟨e₁, rfl⟩ ⟨e₂, rfl⟩651 exact ⟨.sup e₁ e₂, rfl⟩ }652 refine Set.Subset.antisymm ?_ ?_653 · change (VectorSublattice.generated (Set.range x) : Set X) ⊆ (Y : Set X)654 exact VectorSublattice.generated_le (Y := Y) (by655 rintro _ ⟨i, rfl⟩656 exact ⟨.var i, rfl⟩)657 · rintro _ ⟨e, rfl⟩658 induction e with659 | zero =>660 exact (VectorSublattice.generated (Set.range x)).toSubmodule.zero_mem661 | var i =>662 exact VectorSublattice.subset_generated (Set.range x) ⟨i, rfl⟩663 | add e₁ e₂ he₁ he₂ =>664 exact (VectorSublattice.generated (Set.range x)).toSubmodule.add_mem he₁ he₂665 | smul r e he =>666 exact (VectorSublattice.generated (Set.range x)).toSubmodule.smul_mem r he667 | sup e₁ e₂ he₁ he₂ =>668 exact (VectorSublattice.generated (Set.range x)).sup_mem he₁ he₂669 | inf e₁ e₂ he₁ he₂ =>670 exact (VectorSublattice.generated (Set.range x)).inf_mem he₁ he₂671672/-- The sublattice generated by a set `s` coincides with the union, over all673natural numbers `n` and all `n`-tuples `x` with values in `s`, of the sets of674lattice-linear combinations of `x`. -/675theorem generated_eq_iUnion_combinations (s : Set X) :676 (VectorSublattice.generated s : Set X)677 = ⋃ (n : ℕ) (x : Fin n → s), combinations ((↑) ∘ x) := by678 let U : Set X := ⋃ (n : ℕ) (x : Fin n → s), combinations ((↑) ∘ x)679 let Y : VectorSublattice X :=680 { toSubmodule :=681 { carrier := U682 zero_mem' := by683 refine Set.mem_iUnion.mpr ⟨0, ?_⟩684 refine Set.mem_iUnion.mpr ⟨Fin.elim0, ?_⟩685 exact ⟨.zero, rfl⟩686 add_mem' := by687 rintro _ _ hx hy688 simp only [U, Set.mem_iUnion] at hx hy ⊢689 obtain ⟨m, x, e₁, rfl⟩ := hx690 obtain ⟨k, y, e₂, rfl⟩ := hy691 refine ⟨m + k, Fin.append x y, .add (reindexExpr (Fin.castAdd k) e₁)692 (reindexExpr (Fin.natAdd m) e₂), ?_⟩693 simp [Function.comp_def]694 smul_mem' := by695 rintro r _ hx696 simp only [U, Set.mem_iUnion] at hx ⊢697 obtain ⟨m, x, e, rfl⟩ := hx698 exact ⟨m, x, .smul r e, rfl⟩ }699 sup_mem' := by700 rintro _ _ hx hy701 simp only [U, Set.mem_iUnion] at hx hy ⊢702 obtain ⟨m, x, e₁, rfl⟩ := hx703 obtain ⟨k, y, e₂, rfl⟩ := hy704 refine ⟨m + k, Fin.append x y, .sup (reindexExpr (Fin.castAdd k) e₁)705 (reindexExpr (Fin.natAdd m) e₂), ?_⟩706 simp [Function.comp_def] }707 have hsY : s ⊆ Y := by708 intro a ha709 change a ∈ U710 refine Set.mem_iUnion.mpr ⟨1, ?_⟩711 refine Set.mem_iUnion.mpr ⟨(fun _ : Fin 1 => ⟨a, ha⟩), ?_⟩712 exact ⟨.var 0, rfl⟩713 refine Set.Subset.antisymm ?_ ?_714 · exact VectorSublattice.generated_le hsY715 · intro a ha716 simp only [Set.mem_iUnion] at ha717 obtain ⟨m, x, hx⟩ := ha718 have hxgen :719 a ∈720 (VectorSublattice.generated (Set.range ((Subtype.val : s → X) ∘ x)) : Set X) := by721 rwa [generated_range_eq_combinations ((Subtype.val : s → X) ∘ x)]722 exact VectorSublattice.generated_le (Y := VectorSublattice.generated s) (fun y hy => by723 obtain ⟨i, rfl⟩ := hy724 exact VectorSublattice.subset_generated s (x i).2) hxgen725726end Combinations727728end LLexpr729730/-! ### Normed and Banach lattice structure on sublattices -/731732section Normed733734variable {X : Type*} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]735 [NormedVectorLattice X]736737namespace VectorSublattice738739variable (Y : VectorSublattice X)740741/-- A vector sublattice of a normed vector lattice is itself a normed vector742lattice under the induced norm and lattice operations. -/743instance instNormedVectorLatticeSubtype :744 NormedVectorLattice ↥Y.toSubmodule where745 solid := by746 intro x y h747 change ‖x.1‖ ≤ ‖y.1‖748 exact HasSolidNorm.solid h749 norm_smul a x := norm_smul a x.1750751/-- The closure of a vector sublattice in a normed vector lattice is again a752vector sublattice. -/753noncomputable def topologicalClosure (Y : VectorSublattice X) : VectorSublattice X where754 toSubmodule := Y.toSubmodule.topologicalClosure755 sup_mem' := fun {x y} hx hy => by756 have hx' : x ∈ closure (Y.toSubmodule : Set X) := by757 rw [← Submodule.topologicalClosure_coe]; exact hx758 have hy' : y ∈ closure (Y.toSubmodule : Set X) := by759 rw [← Submodule.topologicalClosure_coe]; exact hy760 have hxy : x ⊔ y ∈ closure (Y.toSubmodule : Set X) :=761 map_mem_closure₂ (f := fun a b : X => a ⊔ b)762 NormedVectorLattice.continuous_sup hx' hy'763 (fun _ ha _ hb => Y.sup_mem ha hb)764 rw [← Submodule.topologicalClosure_coe] at hxy765 exact hxy766767end VectorSublattice768769end Normed770771section Banach772773variable {X : Type*} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]774 [BanachLattice X]775776namespace VectorSublattice777778/-- A norm-closed vector sublattice of a Banach lattice is itself a Banach779lattice under the induced structures. -/780@[reducible]781noncomputable def banachLatticeSubtype (Y : VectorSublattice X)782 (hclosed : IsClosed (Y : Set X)) :783 BanachLattice ↥Y.toSubmodule where784 toCompleteSpace := by785 haveI : IsClosed (Y.toSubmodule : Set X) := hclosed786 infer_instance787788end VectorSublattice789790end Banach791792section Normed793794variable {X : Type*} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]795 [NormedVectorLattice X]796797namespace VectorSublattice798799omit [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X] [NormedVectorLattice X] in800/-- Finite subsets of a countable set form a countable set of finsets. -/801private lemma countable_finsets_subset {D : Set X} (hD : D.Countable) :802 {t : Finset X | ↑t ⊆ D}.Countable := by803 classical804 have h_fin : {u : Set X | u.Finite ∧ u ⊆ D}.Countable :=805 Set.countable_setOf_finite_subset hD806 apply Set.Countable.mono ?_ (h_fin.image807 (fun (u : Set X) => if h : u.Finite then h.toFinset else ∅))808 intro t ht809 refine ⟨↑t, ⟨Finset.finite_toSet t, ht⟩, ?_⟩810 simp811812omit [IsOrderedAddMonoid X] [NormedVectorLattice X] in813/-- If `D` is countable, then so is its sup-closure. -/814private lemma countable_supClosure {D : Set X} (hD : D.Countable) :815 (_root_.supClosure D).Countable := by816 classical817 set FD := {t : Finset X | ↑t ⊆ D} with hFD_def818 have hFD : FD.Countable := countable_finsets_subset hD819 apply Set.Countable.mono ?_820 (hFD.image (fun t : Finset X => if h : t.Nonempty then t.sup' h id else (0 : X)))821 intro x hx822 obtain ⟨t, ht, hsub, rfl⟩ := hx823 refine ⟨t, hsub, ?_⟩824 simp [dif_pos ht]825826omit [IsOrderedAddMonoid X] [NormedVectorLattice X] in827/-- If `D` is countable, then so is its inf-closure. -/828private lemma countable_infClosure {D : Set X} (hD : D.Countable) :829 (_root_.infClosure D).Countable := by830 classical831 set FD := {t : Finset X | ↑t ⊆ D} with hFD_def832 have hFD : FD.Countable := countable_finsets_subset hD833 apply Set.Countable.mono ?_834 (hFD.image (fun t : Finset X => if h : t.Nonempty then t.inf' h id else (0 : X)))835 intro x hx836 obtain ⟨t, ht, hsub, rfl⟩ := hx837 refine ⟨t, hsub, ?_⟩838 simp [dif_pos ht]839840/-- If `s ⊆ closure D`, then every element of `supClosure s` belongs to the closure of841`supClosure D`. -/842private lemma supClosure_subset_closure_supClosure {s D : Set X}843 (h : s ⊆ closure D) :844 _root_.supClosure s ⊆ closure (_root_.supClosure D) := by845 intro x hx846 obtain ⟨t, ht, hsub, rfl⟩ := hx847 classical848 have ht_attach : t.attach.Nonempty := Finset.attach_nonempty_iff.mpr ht849 choose f hf_mem hf_tendsto using fun (y : {a // a ∈ t}) =>850 (mem_closure_iff_seq_limit.mp (h (hsub y.property)) :851 ∃ seq, (∀ n, seq n ∈ D) ∧ Filter.Tendsto seq Filter.atTop (nhds y.val))852 set xn : ℕ → X := fun n => t.attach.sup' ht_attach (fun y => f y n)853 have h_sum_mem : ∀ n, xn n ∈ _root_.supClosure D := by854 intro n855 refine ⟨t.attach.image (fun y => f y n), ht_attach.image _, ?_, ?_⟩856 · rintro z hz857 simp only [Finset.coe_image, Set.mem_image] at hz858 obtain ⟨y, _, rfl⟩ := hz859 exact hf_mem y n860 · rw [Finset.sup'_image]861 rfl862 have h_eq : t.attach.sup' ht_attach (Subtype.val : {a // a ∈ t} → X) = t.sup' ht id := by863 refine le_antisymm ?_ ?_864 · exact Finset.sup'_le _ _ fun y _ => Finset.le_sup' (f := id) y.2865 · refine Finset.sup'_le _ _ fun a ha => ?_866 exact Finset.le_sup' (f := Subtype.val) (Finset.mem_attach t ⟨a, ha⟩)867 have h_tendsto : Filter.Tendsto xn Filter.atTop868 (nhds (t.attach.sup' ht_attach (Subtype.val : {a // a ∈ t} → X))) :=869 Filter.Tendsto.finset_sup'_nhds_apply ht_attach (fun y _ => hf_tendsto y)870 rw [← h_eq]871 exact mem_closure_of_tendsto h_tendsto (Filter.Eventually.of_forall h_sum_mem)872873/-- Dual version for inf-closure. -/874private lemma infClosure_subset_closure_infClosure {s D : Set X}875 (h : s ⊆ closure D) :876 _root_.infClosure s ⊆ closure (_root_.infClosure D) := by877 intro x hx878 obtain ⟨t, ht, hsub, rfl⟩ := hx879 classical880 have ht_attach : t.attach.Nonempty := Finset.attach_nonempty_iff.mpr ht881 choose f hf_mem hf_tendsto using fun (y : {a // a ∈ t}) =>882 (mem_closure_iff_seq_limit.mp (h (hsub y.property)) :883 ∃ seq, (∀ n, seq n ∈ D) ∧ Filter.Tendsto seq Filter.atTop (nhds y.val))884 set xn : ℕ → X := fun n => t.attach.inf' ht_attach (fun y => f y n)885 have h_sum_mem : ∀ n, xn n ∈ _root_.infClosure D := by886 intro n887 refine ⟨t.attach.image (fun y => f y n), ht_attach.image _, ?_, ?_⟩888 · rintro z hz889 simp only [Finset.coe_image, Set.mem_image] at hz890 obtain ⟨y, _, rfl⟩ := hz891 exact hf_mem y n892 · rw [Finset.inf'_image]893 rfl894 have h_eq : t.attach.inf' ht_attach (Subtype.val : {a // a ∈ t} → X) = t.inf' ht id := by895 refine le_antisymm ?_ ?_896 · refine Finset.le_inf' _ _ fun a ha => ?_897 exact Finset.inf'_le (f := Subtype.val) (Finset.mem_attach t ⟨a, ha⟩)898 · exact Finset.le_inf' _ _ fun y _ => Finset.inf'_le (f := id) y.2899 have h_tendsto : Filter.Tendsto xn Filter.atTop900 (nhds (t.attach.inf' ht_attach (Subtype.val : {a // a ∈ t} → X))) :=901 Filter.Tendsto.finset_inf'_nhds_apply ht_attach (fun y _ => hf_tendsto y)902 rw [← h_eq]903 exact mem_closure_of_tendsto h_tendsto (Filter.Eventually.of_forall h_sum_mem)904905/-- IsSeparable is preserved under sup-closure in a normed vector lattice. -/906private lemma isSeparable_supClosure {s : Set X}907 (hs : TopologicalSpace.IsSeparable s) :908 TopologicalSpace.IsSeparable (_root_.supClosure s) := by909 obtain ⟨D, hD_ctble, hs_sub⟩ := hs910 exact ⟨_root_.supClosure D, countable_supClosure hD_ctble,911 supClosure_subset_closure_supClosure hs_sub⟩912913/-- IsSeparable is preserved under inf-closure in a normed vector lattice. -/914private lemma isSeparable_infClosure {s : Set X}915 (hs : TopologicalSpace.IsSeparable s) :916 TopologicalSpace.IsSeparable (_root_.infClosure s) := by917 obtain ⟨D, hD_ctble, hs_sub⟩ := hs918 exact ⟨_root_.infClosure D, countable_infClosure hD_ctble,919 infClosure_subset_closure_infClosure hs_sub⟩920921/-- The closed vector sublattice generated by a countable subset of a normed922vector lattice is separable. -/923theorem separableSpace_topologicalClosure_generated_of_countable924 {A : Set X} (hA : A.Countable) :925 TopologicalSpace.SeparableSpace926 ↥(topologicalClosure (generated A)).toSubmodule := by927 have h_span_eq : (generated A : Set X) =928 (generated (Submodule.span ℝ A : Set X) : Set X) := by929 refine Set.Subset.antisymm ?_ ?_930 · exact generated_le (Set.Subset.trans Submodule.subset_span (subset_generated _))931 · exact generated_le932 (Submodule.span_le.mpr (subset_generated A))933 have h_gen : (generated A : Set X) =934 _root_.supClosure (_root_.infClosure (Submodule.span ℝ A : Set X)) := by935 rw [h_span_eq]; exact generated_submodule_eq_supClosure_infClosure _936 have h_span_sep : TopologicalSpace.IsSeparable (Submodule.span ℝ A : Set X) :=937 (hA.isSeparable).span938 have h_gen_sep : TopologicalSpace.IsSeparable (generated A : Set X) := by939 rw [h_gen]940 exact isSeparable_supClosure (isSeparable_infClosure h_span_sep)941 have h_closure_sep : TopologicalSpace.IsSeparable942 ((topologicalClosure (generated A)).toSubmodule : Set X) := by943 have : ((topologicalClosure (generated A)).toSubmodule : Set X) =944 closure (generated A : Set X) := Submodule.topologicalClosure_coe _945 rw [this]946 exact h_gen_sep.closure947 exact h_closure_sep.separableSpace948949end VectorSublattice950951end Normed952