BanLat/Substructures/Band/Generated.lean
All source files · Download exact source
SHA-256: 6bad98d67759be2f88047dfaf9192864ce60bb7790e659eba1cd844ce152273d
1/-2Authors: David Muñoz-Lahoz3-/45import BanLat.Substructures.Band.DisjointComplement6import BanLat.Substructures.Band.Lattice78/-!9# The band generated by a set1011The band generated by a set `s ⊆ X` is the smallest band of `X` containing12`s`, obtained as the infimum of all bands containing `s`.1314In an Archimedean vector lattice the double disjoint complement `Aᵈᵈ`15coincides with the band generated by `A`. As consequences we obtain four16equivalent descriptions of the band generated by an order ideal in terms of17suprema, a concrete description of the principal band as the supremum of18the increasing sequence `x ⊓ n • a`, and the characterisation of weak19order units as those non-negative elements that generate the whole space20as a band. As another consequence, every band of a normed vector lattice is21norm closed.22-/2324variable {X : Type*} [AddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]25 [VectorLattice X]2627namespace Band2829/-- The band generated by a set `s`: the smallest band of `X` containing30`s`. -/31def generated (s : Set X) : Band X :=32 sInf {B : Band X | s ⊆ B}3334/-- The generating set is contained in the band it generates. -/35theorem subset_generated (s : Set X) : s ⊆ (generated s : Set X) := by36 intro x hx37 rw [SetLike.mem_coe, generated, mem_sInf]38 exact fun B hB => hB hx3940/-- The band generated by `s` is contained in every band containing `s`. -/41theorem generated_le {s : Set X} {B : Band X} (h : s ⊆ B) :42 generated s ≤ B :=43 sInf_le h4445/-! ### Characterisation of bands via disjoint complements -/4647omit [VectorLattice X] in48private lemma posPart_mem_dd {A : Set X}49 {x : X} (hx : x ∈ Aᵈᵈ) : x⁺ ∈ Aᵈᵈ := fun a ha =>50 (hx a ha).mono_left (by51 rw [abs_of_nonneg (posPart_nonneg x)]52 exact sup_le (le_abs_self x) (abs_nonneg x))5354omit [VectorLattice X] in55private lemma negPart_mem_dd {A : Set X}56 {x : X} (hx : x ∈ Aᵈᵈ) : x⁻ ∈ Aᵈᵈ := fun a ha =>57 (hx a ha).mono_left (by58 rw [abs_of_nonneg (negPart_nonneg x)]59 exact sup_le (neg_le_abs x) (abs_nonneg x))6061omit [VectorLattice X] in62private lemma solid_dd {A : Set X} {x y : X}63 (hx : x ∈ Aᵈᵈ) (h : |y| ≤ |x|) : y ∈ Aᵈᵈ := fun a ha =>64 (hx a ha).mono_left h6566private lemma archimedean_disjoint_step [IsVLArchimedean X]67 {v t w : X} (hv_nn : 0 ≤ v) (ht_nn : 0 ≤ t) (hw_nn : 0 ≤ w)68 (ht_le_v : t ≤ v) (hbound : ∀ n : ℕ, v ⊓ (n • t - w) ≤ 0) : t = 0 := by69 letI : DistribLattice X := AddCommGroup.toDistribLattice X70 refine IsVLArchimedean.eq_zero_of_nonneg_of_forall_nsmul_le (y := w) ht_nn71 (fun n => ?_)72 have h_nv_nn : (0 : X) ≤ n • v := nsmul_nonneg hv_nn n73 have h_nt_le_nv : n • t ≤ n • v := nsmul_le_nsmul_right ht_le_v n74 have hkey1 : v ⊓ (n • t - w)⁺ = 0 := by75 refine le_antisymm ?_ (le_inf hv_nn (posPart_nonneg _))76 calc v ⊓ (n • t - w)⁺77 = v ⊓ ((n • t - w) ⊔ 0) := by rw [posPart_def]78 _ = (v ⊓ (n • t - w)) ⊔ (v ⊓ 0) := inf_sup_left v _ _79 _ ≤ 0 := sup_le (hbound n) (by rw [inf_of_le_right hv_nn])80 have hkey2 : (n • t - w)⁺ ⊓ (n • v) = 0 := by81 have hdisj : IsVLDisjoint (n • t - w)⁺ v := by82 change |(n • t - w)⁺| ⊓ |v| = 083 rw [abs_of_nonneg (posPart_nonneg _), abs_of_nonneg hv_nn, inf_comm]84 exact hkey185 have hdisj_n : IsVLDisjoint (n • t - w)⁺ ((n : ℝ) • v) :=86 hdisj.smul_right (n : ℝ)87 have hh : |(n • t - w)⁺| ⊓ |(n : ℝ) • v| = 0 := hdisj_n88 rw [abs_of_nonneg (posPart_nonneg _),89 abs_of_nonneg (smul_nonneg (Nat.cast_nonneg n) hv_nn)] at hh90 rw [show (n • v : X) = ((n : ℝ) • v) from (Nat.cast_smul_eq_nsmul ℝ n v).symm]91 exact hh92 have hpos_le_nt : (n • t - w)⁺ ≤ n • t :=93 sup_le (sub_le_self _ hw_nn) (nsmul_nonneg ht_nn n)94 have hpos_le_nv : (n • t - w)⁺ ≤ n • v := hpos_le_nt.trans h_nt_le_nv95 have hpos_zero : (n • t - w)⁺ = 0 := by96 have : (n • t - w)⁺ = (n • t - w)⁺ ⊓ (n • v) :=97 (inf_eq_left.mpr hpos_le_nv).symm98 exact this.trans hkey299 have h_le : n • t - w ≤ 0 := posPart_eq_zero.mp hpos_zero100 exact sub_nonpos.mp h_le101102/-- The hard direction: in an Archimedean vector lattice, a non-negative103element of `Aᵈᵈ` lies in the band generated by `A`. -/104private lemma mem_generated_of_nonneg_of_mem_ddc [IsVLArchimedean X]105 (A : Set X) {x : X} (hx : 0 ≤ x) (hxAdd : x ∈ Aᵈᵈ) :106 x ∈ Band.generated A := by107 set G : Band X := Band.generated A with hG_def108 have hAG : A ⊆ (G : Set X) := subset_generated A109 -- It suffices to show `IsLUB (G ∩ [0, x]) x`, since `G` is a band.110 suffices h : IsLUB ((G.toOrderIdeal : Set X) ∩ Set.Icc 0 x) x by111 refine G.sSup_mem (S := (G.toOrderIdeal : Set X) ∩ Set.Icc 0 x)112 (fun y hy => hy.1)113 ⟨0, G.toOrderIdeal.toSubmodule.zero_mem, le_refl 0, hx⟩ h114 refine ⟨fun b hb => hb.2.2, ?_⟩115 intro u hu116 have hu_nn : 0 ≤ u := hu ⟨G.toOrderIdeal.toSubmodule.zero_mem, le_refl 0, hx⟩117 set v : X := (x - u)⁺ with hv_def118 have hv_nn : 0 ≤ v := posPart_nonneg _119 have hv_le_x : v ≤ x := sup_le (sub_le_self _ hu_nn) hx120 have hv_Add : v ∈ Aᵈᵈ :=121 solid_dd hxAdd (by rw [abs_of_nonneg hv_nn, abs_of_nonneg hx]; exact hv_le_x)122 have hv_Ad : v ∈ Aᵈ := by123 intro a ha124 set t : X := v ⊓ |a| with ht_def125 have ht_nn : 0 ≤ t := le_inf hv_nn (abs_nonneg _)126 have ht_le_v : t ≤ v := inf_le_left127 have ht_le_abs : t ≤ |a| := inf_le_right128 have habs_G : |a| ∈ G := G.abs_mem (hAG ha)129 have ht_G : t ∈ G := G.solid habs_G ht_nn ht_le_abs130 set w : X := x ⊓ u with hw_def131 have hbound : ∀ n : ℕ, v ⊓ (n • t - w) ≤ 0 := by132 intro n133 have hnt_G : n • t ∈ G := G.toSubmodule.nsmul_mem ht_G n134 have hnt_nn : 0 ≤ n • t := nsmul_nonneg ht_nn n135 have hxnt_G : x ⊓ n • t ∈ G :=136 G.solid hnt_G (le_inf hx hnt_nn) inf_le_right137 have hxnt_le_x : x ⊓ n • t ≤ x := inf_le_left138 have hxnt_le_u : x ⊓ n • t ≤ u :=139 hu ⟨hxnt_G, le_inf hx hnt_nn, hxnt_le_x⟩140 have hxnt_le_w : x ⊓ n • t ≤ w := le_inf hxnt_le_x hxnt_le_u141 have hv_eq : v = x - w := by rw [hv_def, hw_def, sub_inf_eq_posPart]142 have h1 : v ⊓ (n • t - w) = x ⊓ n • t - w := by143 rw [hv_eq, ← inf_sub]144 rw [h1]145 exact sub_nonpos.mpr hxnt_le_w146 have hw_nn : 0 ≤ w := le_inf hx hu_nn147 have ht_zero : t = 0 :=148 archimedean_disjoint_step hv_nn ht_nn hw_nn ht_le_v hbound149 change |v| ⊓ |a| = 0150 rw [abs_of_nonneg hv_nn]151 exact ht_zero152 have hv_zero : v = 0 :=153 disjointComplement_inter_eq_zero Aᵈ ⟨hv_Ad, hv_Add⟩154 have hxu : (x - u)⁺ = 0 := hv_zero155 rw [posPart_eq_zero, sub_nonpos] at hxu156 exact hxu157158/-- In an Archimedean vector lattice, the double disjoint complement of a set159equals the band it generates. -/160theorem disjointComplement_disjointComplement_eq_generated161 [IsVLArchimedean X] (A : Set X) :162 ((Aᵈ)ᵈ : Set X) = (generated A : Set X) := by163 apply Set.Subset.antisymm164 · intro x hx165 have hxp : x⁺ ∈ Band.generated A :=166 mem_generated_of_nonneg_of_mem_ddc A (posPart_nonneg x) (posPart_mem_dd hx)167 have hxn : x⁻ ∈ Band.generated A :=168 mem_generated_of_nonneg_of_mem_ddc A (negPart_nonneg x) (negPart_mem_dd hx)169 have := (Band.generated A).toSubmodule.sub_mem hxp hxn170 rwa [posPart_sub_negPart] at this171 · exact generated_le (B := Band.disjointComplement Aᵈ)172 (subset_disjointComplement_disjointComplement A)173174/-- The band generated by a set together with its disjoint complement is the175whole space. -/176theorem generated_union_disjointComplement_eq_top [IsVLArchimedean X] (A : Set X) :177 generated (A ∪ Aᵈ) = (⊤ : Band X) := by178 apply le_antisymm179 · exact le_top180 · intro x _181 have hx : x ∈ ((A ∪ Aᵈ)ᵈ)ᵈ := by182 rw [disjointComplement_union_disjointComplement_eq_singleton A]183 intro a ha184 rw [Set.mem_singleton_iff.mp ha]185 exact isVLDisjoint_zero_right x186 rwa [disjointComplement_disjointComplement_eq_generated] at hx187188/-- In an Archimedean vector lattice, every band equals its double disjoint189complement. -/190theorem eq_disjointComplement_disjointComplement [IsVLArchimedean X]191 (B : Band X) : ((↑B : Set X)ᵈ)ᵈ = ↑B := by192 rw [disjointComplement_disjointComplement_eq_generated]193 exact congrArg _ (le_antisymm (generated_le (fun _ h => h)) (subset_generated _))194195/-- In an Archimedean vector lattice, every band is the disjoint complement of196some set. -/197theorem exists_eq_disjointComplement [IsVLArchimedean X] (B : Band X) :198 ∃ A : Set X, Aᵈ = ↑B :=199 ⟨(B : Set X)ᵈ, eq_disjointComplement_disjointComplement B⟩200201/-! ### Description of the band generated by an ideal202203For an order ideal `J`, the positive part of the band generated by `J`204admits four equivalent descriptions: it consists of those non-negative205elements `x` that are the supremum of an upward-directed net in `J`,206equivalently, the supremum of a non-empty set of non-negative elements207of `J`, equivalently, the supremum of `J ∩ [0, x]`. -/208209/-- Backward direction: if `IsLUB D x` for some non-empty `D ⊆ J`, then `x`210belongs to the band generated by `J`. -/211private lemma mem_generated_of_isLUB_subset {J : OrderIdeal X} {x : X}212 {D : Set X} (hne : D.Nonempty) (hDJ : D ⊆ (J : Set X)) (hx : IsLUB D x) :213 x ∈ generated (J : Set X) :=214 (generated (J : Set X)).sSup_mem215 (fun _ hy => subset_generated _ (hDJ hy)) hne hx216217/-- Forward direction (Archimedean): if `0 ≤ x` belongs to the band generated218by an order ideal `J`, then `x` is the supremum of `J ∩ [0, x]`. -/219private lemma isLUB_inter_of_mem_generated_orderIdeal [IsVLArchimedean X]220 (J : OrderIdeal X) {x : X} (hx : 0 ≤ x)221 (hxG : x ∈ generated (J : Set X)) :222 IsLUB ((J : Set X) ∩ Set.Icc 0 x) x := by223 have hxAdd : x ∈ ((J : Set X)ᵈ)ᵈ := by224 rw [disjointComplement_disjointComplement_eq_generated]; exact hxG225 refine ⟨fun b hb => hb.2.2, ?_⟩226 intro u hu227 have hu_nn : 0 ≤ u := hu ⟨J.toSubmodule.zero_mem, le_refl 0, hx⟩228 set v : X := (x - u)⁺ with hv_def229 have hv_nn : 0 ≤ v := posPart_nonneg _230 have hv_le_x : v ≤ x := sup_le (sub_le_self _ hu_nn) hx231 have hv_Add : v ∈ ((J : Set X)ᵈ)ᵈ :=232 solid_dd hxAdd (by rw [abs_of_nonneg hv_nn, abs_of_nonneg hx]; exact hv_le_x)233 have hv_Ad : v ∈ ((J : Set X))ᵈ := by234 intro a ha235 set t : X := v ⊓ |a| with ht_def236 have ht_nn : 0 ≤ t := le_inf hv_nn (abs_nonneg _)237 have ht_le_v : t ≤ v := inf_le_left238 have ht_le_abs : t ≤ |a| := inf_le_right239 have habs_J : |a| ∈ J := J.abs_mem ha240 set w : X := x ⊓ u with hw_def241 have hbound : ∀ n : ℕ, v ⊓ (n • t - w) ≤ 0 := by242 intro n243 have hnabs_J : n • |a| ∈ J := J.toSubmodule.nsmul_mem habs_J n244 have hnabs_nn : 0 ≤ n • |a| := nsmul_nonneg (abs_nonneg _) n245 have hnt_le_nabs : n • t ≤ n • |a| := nsmul_le_nsmul_right ht_le_abs n246 have hxnt_le_xnabs : x ⊓ n • t ≤ x ⊓ n • |a| :=247 inf_le_inf_left _ hnt_le_nabs248 have hxnabs_J : x ⊓ n • |a| ∈ J :=249 J.solid hnabs_J (le_inf hx hnabs_nn) inf_le_right250 have hxnabs_le_x : x ⊓ n • |a| ≤ x := inf_le_left251 have hxnabs_le_u : x ⊓ n • |a| ≤ u :=252 hu ⟨hxnabs_J, le_inf hx hnabs_nn, hxnabs_le_x⟩253 have hxnt_le_x : x ⊓ n • t ≤ x := inf_le_left254 have hxnt_le_u : x ⊓ n • t ≤ u := hxnt_le_xnabs.trans hxnabs_le_u255 have hxnt_le_w : x ⊓ n • t ≤ w := le_inf hxnt_le_x hxnt_le_u256 have hv_eq : v = x - w := by rw [hv_def, hw_def, sub_inf_eq_posPart]257 have h1 : v ⊓ (n • t - w) = x ⊓ n • t - w := by258 rw [hv_eq, ← inf_sub]259 rw [h1]260 exact sub_nonpos.mpr hxnt_le_w261 have hw_nn : 0 ≤ w := le_inf hx hu_nn262 have ht_zero : t = 0 :=263 archimedean_disjoint_step hv_nn ht_nn hw_nn ht_le_v hbound264 change |v| ⊓ |a| = 0265 rw [abs_of_nonneg hv_nn]; exact ht_zero266 have hv_zero : v = 0 :=267 disjointComplement_inter_eq_zero (J : Set X)ᵈ ⟨hv_Ad, hv_Add⟩268 have hxu : (x - u)⁺ = 0 := hv_zero269 rw [posPart_eq_zero, sub_nonpos] at hxu270 exact hxu271272/-- For an order ideal `J` and a non-negative element `x`, `x` belongs to273the band generated by `J` iff `x` is the supremum of an upward-directed274non-empty set of non-negative elements of `J`. -/275theorem mem_generated_orderIdeal_iff_isLUB_directed [IsVLArchimedean X]276 (J : OrderIdeal X) {x : X} (hx : 0 ≤ x) :277 x ∈ generated (J : Set X) ↔278 ∃ S : Set X, S.Nonempty ∧ S ⊆ (J : Set X) ∧ (∀ y ∈ S, 0 ≤ y)279 ∧ DirectedOn (· ≤ ·) S ∧ IsLUB S x := by280 refine ⟨fun hxG => ?_, ?_⟩281 · refine ⟨(J : Set X) ∩ Set.Icc 0 x,282 ⟨0, J.toSubmodule.zero_mem, le_refl 0, hx⟩,283 fun _ hy => hy.1, fun _ hy => hy.2.1, ?_, ?_⟩284 · rintro a ⟨haJ, ha0, hax⟩ b ⟨hbJ, _, hbx⟩285 exact ⟨a ⊔ b, ⟨J.sup_mem haJ hbJ, le_sup_of_le_left ha0, sup_le hax hbx⟩,286 le_sup_left, le_sup_right⟩287 · exact isLUB_inter_of_mem_generated_orderIdeal J hx hxG288 · rintro ⟨S, hne, hSJ, _, _, hx⟩289 exact mem_generated_of_isLUB_subset hne hSJ hx290291/-- For an order ideal `J` and a non-negative element `x`, `x` belongs to292the band generated by `J` iff `x` is the supremum of a non-empty set of293non-negative elements of `J`. -/294theorem mem_generated_orderIdeal_iff_isLUB_nonneg [IsVLArchimedean X]295 (J : OrderIdeal X) {x : X} (hx : 0 ≤ x) :296 x ∈ generated (J : Set X) ↔297 ∃ D : Set X, D.Nonempty ∧ D ⊆ (J : Set X) ∧ (∀ y ∈ D, 0 ≤ y)298 ∧ IsLUB D x := by299 refine ⟨fun hxG => ?_, ?_⟩300 · refine ⟨(J : Set X) ∩ Set.Icc 0 x,301 ⟨0, J.toSubmodule.zero_mem, le_refl 0, hx⟩,302 fun _ hy => hy.1, fun _ hy => hy.2.1, ?_⟩303 exact isLUB_inter_of_mem_generated_orderIdeal J hx hxG304 · rintro ⟨D, hne, hDJ, _, hx⟩305 exact mem_generated_of_isLUB_subset hne hDJ hx306307/-- For an order ideal `J` and a non-negative element `x`, `x` belongs to308the band generated by `J` iff `x` is the supremum of `J ∩ [0, x]`. -/309theorem mem_generated_orderIdeal_iff_isLUB_inter [IsVLArchimedean X]310 (J : OrderIdeal X) {x : X} (hx : 0 ≤ x) :311 x ∈ generated (J : Set X) ↔312 IsLUB ((J : Set X) ∩ Set.Icc 0 x) x := by313 refine ⟨isLUB_inter_of_mem_generated_orderIdeal J hx, fun h => ?_⟩314 exact mem_generated_of_isLUB_subset (D := (J : Set X) ∩ Set.Icc 0 x)315 ⟨0, J.toSubmodule.zero_mem, le_refl 0, hx⟩316 (fun _ hy => hy.1) h317318/-! ### Description of the principal band319320The band generated by a single non-negative element `a` admits a concrete321description: a non-negative `x` belongs to it iff `x` is the supremum of322the increasing sequence `x ⊓ n • a` for `n ∈ ℕ`. -/323324/-- Forward direction (Archimedean): if `0 ≤ x` belongs to the band generated325by `{a}` for some `0 ≤ a`, then `x` is the supremum of `x ⊓ n • a`. -/326private lemma isLUB_inf_nsmul_of_mem_generated_singleton [IsVLArchimedean X]327 {a x : X} (ha : 0 ≤ a) (hx : 0 ≤ x)328 (hxG : x ∈ generated ({a} : Set X)) :329 IsLUB (Set.range fun n : ℕ => x ⊓ n • a) x := by330 have hxAdd : x ∈ (({a} : Set X)ᵈ)ᵈ := by331 rw [disjointComplement_disjointComplement_eq_generated]; exact hxG332 refine ⟨?_, ?_⟩333 · rintro _ ⟨_, rfl⟩; exact inf_le_left334 intro u hu335 have h0 : x ⊓ (0 : ℕ) • a = 0 := by336 rw [zero_nsmul]; exact inf_of_le_right hx337 have hu_nn : 0 ≤ u := h0 ▸ hu ⟨0, rfl⟩338 set v : X := (x - u)⁺ with hv_def339 have hv_nn : 0 ≤ v := posPart_nonneg _340 have hv_le_x : v ≤ x := sup_le (sub_le_self _ hu_nn) hx341 have hv_Add : v ∈ (({a} : Set X)ᵈ)ᵈ :=342 solid_dd hxAdd (by rw [abs_of_nonneg hv_nn, abs_of_nonneg hx]; exact hv_le_x)343 have hv_Ad : v ∈ (({a} : Set X))ᵈ := by344 rintro b rfl345 set t : X := v ⊓ |b| with ht_def346 have ht_nn : 0 ≤ t := le_inf hv_nn (abs_nonneg _)347 have ht_le_v : t ≤ v := inf_le_left348 have ht_le_abs : t ≤ |b| := inf_le_right349 have habs_eq : |b| = b := abs_of_nonneg ha350 set w : X := x ⊓ u with hw_def351 have hbound : ∀ n : ℕ, v ⊓ (n • t - w) ≤ 0 := by352 intro n353 have ht_le_b : t ≤ b := habs_eq ▸ ht_le_abs354 have hnt_le_nb : n • t ≤ n • b := nsmul_le_nsmul_right ht_le_b n355 have hxnt_le_xnb : x ⊓ n • t ≤ x ⊓ n • b :=356 inf_le_inf_left _ hnt_le_nb357 have hxnb_le_u : x ⊓ n • b ≤ u := hu ⟨n, rfl⟩358 have hxnt_le_x : x ⊓ n • t ≤ x := inf_le_left359 have hxnt_le_u : x ⊓ n • t ≤ u := hxnt_le_xnb.trans hxnb_le_u360 have hxnt_le_w : x ⊓ n • t ≤ w := le_inf hxnt_le_x hxnt_le_u361 have hv_eq : v = x - w := by rw [hv_def, hw_def, sub_inf_eq_posPart]362 have h1 : v ⊓ (n • t - w) = x ⊓ n • t - w := by363 rw [hv_eq, ← inf_sub]364 rw [h1]365 exact sub_nonpos.mpr hxnt_le_w366 have hw_nn : 0 ≤ w := le_inf hx hu_nn367 have ht_zero : t = 0 :=368 archimedean_disjoint_step hv_nn ht_nn hw_nn ht_le_v hbound369 change |v| ⊓ |b| = 0370 rw [abs_of_nonneg hv_nn]; exact ht_zero371 have hv_zero : v = 0 :=372 disjointComplement_inter_eq_zero ({a} : Set X)ᵈ ⟨hv_Ad, hv_Add⟩373 have hxu : (x - u)⁺ = 0 := hv_zero374 rw [posPart_eq_zero, sub_nonpos] at hxu375 exact hxu376377/-- For non-negative `a` and `x`, `x` belongs to the band generated by378`{a}` iff `x` is the supremum of the sequence `x ⊓ n • a`. -/379theorem mem_generated_singleton_iff_isLUB_inf_nsmul [IsVLArchimedean X]380 {a x : X} (ha : 0 ≤ a) (hx : 0 ≤ x) :381 x ∈ generated ({a} : Set X) ↔382 IsLUB (Set.range fun n : ℕ => x ⊓ n • a) x := by383 refine ⟨isLUB_inf_nsmul_of_mem_generated_singleton ha hx, fun h => ?_⟩384 set G : Band X := generated ({a} : Set X) with hG_def385 have ha_G : a ∈ G := subset_generated _ rfl386 refine G.sSup_mem (S := Set.range fun n : ℕ => x ⊓ n • a) ?_387 (Set.range_nonempty _) h388 rintro _ ⟨n, rfl⟩389 have hna_G : n • a ∈ G := G.toSubmodule.nsmul_mem ha_G n390 have hna_nn : 0 ≤ n • a := nsmul_nonneg ha n391 exact G.solid hna_G (le_inf hx hna_nn) inf_le_right392393end Band394395/-! ### Weak order units -/396397/-- In an Archimedean vector lattice, a non-negative element `e` is a weak398order unit iff the band it generates is the whole space. -/399theorem weakOrderUnit_iff_generated_singleton_eq_top [IsVLArchimedean X]400 {e : X} (he : 0 ≤ e) :401 WeakOrderUnit e ↔ Band.generated {e} = ⊤ := by402 constructor403 · rintro ⟨_, hwou⟩404 apply SetLike.coe_set_eq.mp405 rw [← Band.disjointComplement_disjointComplement_eq_generated]406 show ((({e} : Set X)ᵈ)ᵈ : Set X) = (⊤ : Band X)407 ext x408 refine ⟨fun _ => trivial, fun _ y hy => ?_⟩409 have hye : IsVLDisjoint y e := hy e rfl410 rw [hwou y hye]411 exact isVLDisjoint_zero_right x412 · intro htop413 refine ⟨he, fun x hxe => ?_⟩414 have hx_in : x ∈ ((↑(Band.generated ({e} : Set X)) : Set X)) := by415 rw [show Band.generated ({e} : Set X) = ⊤ from htop]; trivial416 rw [← Band.disjointComplement_disjointComplement_eq_generated] at hx_in417 have hxe' : x ∈ ({e} : Set X)ᵈ := fun a ha => by418 rcases ha with rfl; exact hxe419 have hx_self : IsVLDisjoint x x :=420 isVLDisjoint_comm.mp (hx_in x hxe')421 have h : |x| ⊓ |x| = 0 := hx_self422 rw [inf_idem] at h423 exact (abs_eq_zero_iff_zero x).mp h424425/-! ### Closedness in normed vector lattices -/426427section Normed428429variable {X : Type*} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]430 [NormedVectorLattice X]431432namespace Band433434variable (B : Band X)435436/-- Every band of a normed vector lattice is norm closed: it equals its double437disjoint complement, which is closed. -/438theorem isClosed_coe : IsClosed ((B : Set X)) := by439 rw [← Band.eq_disjointComplement_disjointComplement B]440 exact isClosed_disjointComplement _441442/-- The underlying submodule of a band of a normed vector lattice is norm443closed. -/444theorem isClosed_toSubmodule : IsClosed ((B.toSubmodule : Set X)) := isClosed_coe B445446end Band447448end Normed449450section Banach451452variable {X : Type*} [NormedAddCommGroup X] [Lattice X] [IsOrderedAddMonoid X]453 [BanachLattice X]454455namespace Band456457variable (B : Band X)458459/-- A band of a Banach lattice, equipped with the inherited normed vector460lattice structure, is itself a Banach lattice. -/461noncomputable instance instBanachLatticeSubtype :462 BanachLattice ↥B.toSubmodule :=463 VectorSublattice.banachLatticeSubtype B.toVectorSublattice B.isClosed_coe464465end Band466467end Banach468