PointwisePrefixes.lean

1import BFPP.PointwiseSupremum23/-! # Algebra of increasing pointwise prefixes -/45namespace BFPP67set_option autoImplicit false8open Set Order Cardinal unitInterval910universe u v w11variable {K : Type u} [TopologicalSpace K]12variable {ι : Type v} [LinearOrder ι]1314noncomputable def pointwisePrefix (g : ι → C(K, I)) (i : ι) (t : K) : I := ⨆ j < i, g j t1516theorem pointwisePrefix_image (g : ι → C(K, I)) (i : ι) :17    pointwisePrefix g i = pointwiseSup (g '' Iio i) := by18  funext t19  simp only [pointwisePrefix, pointwiseSup, iSup_image, mem_Iio]2021theorem pointwisePrefix_mono (g : ι → C(K, I)) : Monotone (pointwisePrefix g) := by22  intro i j hij t23  exact iSup_le fun k => iSup_le fun hk =>24    le_iSup_of_le k (le_iSup_of_le (hk.trans_le hij) le_rfl)2526theorem pointwisePrefix_bot [OrderBot ι] (g : ι → C(K, I)) :27    pointwisePrefix g ⊥ = fun _ => 0 := by28  funext t29  simp only [pointwisePrefix, not_lt_bot, iSup_false, iSup_bot]30  rfl3132theorem pointwisePrefix_limit (g : ι → C(K, I)) (i : ι)33    (hi : ∀ j, j < i → ∃ k, j < k ∧ k < i) (t : K) :34    pointwisePrefix g i t = ⨆ j : Iio i, pointwisePrefix g j.val t := by35  apply le_antisymm36  · refine iSup_le fun j => iSup_le fun hj => ?_37    obtain ⟨k, hjk, hki⟩ := hi j hj38    exact le_iSup_of_le ⟨k, hki⟩ (le_iSup_of_le j (le_iSup_of_le hjk le_rfl))39  · exact iSup_le fun j => pointwisePrefix_mono g j.property.le t4041theorem pointwisePrefix_terminal [NoMaxOrder ι] (g : ι → C(K, I)) (t : K) :42    (⨆ i, pointwisePrefix g i t) = ⨆ i, g i t := by43  apply le_antisymm44  · exact iSup_le fun i => iSup_le fun j => iSup_le fun _ => le_iSup (fun j => g j t) j45  · refine iSup_le fun j => ?_46    obtain ⟨i, hji⟩ := exists_gt j47    exact le_iSup_of_le i (le_iSup_of_le j (le_iSup_of_le hji le_rfl))4849theorem pointwisePrefix_reindex {ν : Type w} [LinearOrder ν] (e : ν ≃o ι)50    (g : ι → C(K, I)) (i : ν) :51    pointwisePrefix (g ∘ e) i = pointwisePrefix g (e i) := by52  funext t53  apply le_antisymm54  · refine iSup_le fun j => iSup_le fun hj => ?_55    exact le_iSup_of_le (e j) (le_iSup_of_le (e.strictMono hj) le_rfl)56  · refine iSup_le fun j => iSup_le fun hj => ?_57    have hji : e.symm j < i := by simpa using e.symm.strictMono hj58    exact le_iSup_of_le (e.symm j) (le_iSup_of_le hji (by simp))5960end BFPP

SHA-256