feat(measure_theory/construction/borel_space): two measures are equal…

… if they agree on closed-open intervals (#9396)

Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>

src/data/set/intervals/disjoint.lean

@@ -60,6 +60,22 @@ begin
   exact h.elim (λ h, absurd hx (not_lt_of_le h)) id
 end
 
+@[simp] lemma Union_Ico_eq_Iio_self_iff {ι : Sort*} {f : ι → α} {a : α} :
+  (⋃ i, Ico (f i) a) = Iio a ↔ ∀ x < a, ∃ i, f i ≤ x :=
+by simp [← Ici_inter_Iio, ← Union_inter, subset_def]
+
+@[simp] lemma Union_Ioc_eq_Ioi_self_iff {ι : Sort*} {f : ι → α} {a : α} :
+  (⋃ i, Ioc a (f i)) = Ioi a ↔ ∀ x, a < x → ∃ i, x ≤ f i :=
+by simp [← Ioi_inter_Iic, ← inter_Union, subset_def]
+
+@[simp] lemma bUnion_Ico_eq_Iio_self_iff {ι : Sort*} {p : ι → Prop} {f : Π i, p i → α} {a : α} :
+  (⋃ i (hi : p i), Ico (f i hi) a) = Iio a ↔ ∀ x < a, ∃ i hi, f i hi ≤ x :=
+by simp [← Ici_inter_Iio, ← Union_inter, subset_def]
+
+@[simp] lemma bUnion_Ioc_eq_Ioi_self_iff {ι : Sort*} {p : ι → Prop} {f : Π i, p i → α} {a : α} :
+  (⋃ i (hi : p i), Ioc a (f i hi)) = Ioi a ↔ ∀ x, a < x → ∃ i hi, x ≤ f i hi :=
+by simp [← Ioi_inter_Iic, ← inter_Union, subset_def]
+
 end linear_order
 
 end set

src/data/set/lattice.lean

@@ -522,11 +522,8 @@ end
 
 theorem bInter_mono' {s s' : set α} {t t' : α → set β} (hs : s ⊆ s') (h : ∀ x ∈ s, t x ⊆ t' x) :
   (⋂ x ∈ s', t x) ⊆ (⋂ x ∈ s, t' x) :=
-begin
-  intros x x_in,
-  simp only [mem_Inter] at *,
-  exact λ a a_in, h a a_in $ x_in _ (hs a_in)
-end
+(bInter_subset_bInter_left hs).trans $
+  subset_bInter (λ x xs, subset.trans (bInter_subset_of_mem xs) (h x xs))
 
 theorem bInter_mono {s : set α} {t t' : α → set β} (h : ∀ x ∈ s, t x ⊆ t' x) :
   (⋂ x ∈ s, t x) ⊆ (⋂ x ∈ s, t' x) :=

src/measure_theory/measurable_space.lean

@@ -126,7 +126,7 @@ lemma le_map_comap : m ≤ (m.comap g).map g := (gc_comap_map g).le_u_l _
 
 end functors
 
-lemma generate_from_le_generate_from {s t : set (set α)} (h : s ⊆ t) :
+@[mono] lemma generate_from_mono {s t : set (set α)} (h : s ⊆ t) :
   generate_from s ≤ generate_from t :=
 gi_generate_from.gc.monotone_l h
 

src/measure_theory/measure/stieltjes.lean

@@ -266,7 +266,7 @@ end
 
 lemma borel_le_measurable : borel ℝ ≤ f.outer.caratheodory :=
 begin
-  rw borel_eq_generate_Ioi,
+  rw borel_eq_generate_from_Ioi,
   refine measurable_space.generate_from_le _,
   simp [f.measurable_set_Ioi] { contextual := tt }
 end

src/measure_theory/pi_system.lean

@@ -73,6 +73,76 @@ begin
       set.mem_singleton_iff],
 end
 
+section order
+
+variables {α : Type*} {ι ι' : Sort*} [linear_order α]
+
+lemma is_pi_system_image_Iio (s : set α) : is_pi_system (Iio '' s) :=
+begin
+  rintro _ _ ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩ -,
+  exact ⟨a ⊓ b, inf_ind a b ha hb, Iio_inter_Iio.symm⟩
+end
+
+lemma is_pi_system_Iio : is_pi_system (range Iio : set (set α)) :=
+@image_univ α _ Iio ▸ is_pi_system_image_Iio univ
+
+lemma is_pi_system_image_Ioi (s : set α) : is_pi_system (Ioi '' s) :=
+@is_pi_system_image_Iio (order_dual α) _ s
+
+lemma is_pi_system_Ioi : is_pi_system (range Ioi : set (set α)) :=
+@image_univ α _ Ioi ▸ is_pi_system_image_Ioi univ
+
+lemma is_pi_system_Ixx_mem {Ixx : α → α → set α} {p : α → α → Prop}
+  (Hne : ∀ {a b}, (Ixx a b).nonempty → p a b)
+  (Hi : ∀ {a₁ b₁ a₂ b₂}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂)) (s t : set α) :
+  is_pi_system {S | ∃ (l ∈ s) (u ∈ t) (hlu : p l u), Ixx l u = S} :=
+begin
+  rintro _ _ ⟨l₁, hls₁, u₁, hut₁, hlu₁, rfl⟩ ⟨l₂, hls₂, u₂, hut₂, hlu₂, rfl⟩,
+  simp only [Hi, ← sup_eq_max, ← inf_eq_min],
+  exact λ H, ⟨l₁ ⊔ l₂, sup_ind l₁ l₂ hls₁ hls₂, u₁ ⊓ u₂, inf_ind u₁ u₂ hut₁ hut₂, Hne H, rfl⟩
+end
+
+lemma is_pi_system_Ixx {Ixx : α → α → set α} {p : α → α → Prop}
+  (Hne : ∀ {a b}, (Ixx a b).nonempty → p a b)
+  (Hi : ∀ {a₁ b₁ a₂ b₂}, Ixx a₁ b₁ ∩ Ixx a₂ b₂ = Ixx (max a₁ a₂) (min b₁ b₂))
+  (f : ι → α) (g : ι' → α) :
+  @is_pi_system α ({S | ∃ i j (h : p (f i) (g j)), Ixx (f i) (g j) = S}) :=
+by simpa only [exists_range_iff] using is_pi_system_Ixx_mem @Hne @Hi (range f) (range g)
+
+lemma is_pi_system_Ioo_mem (s t : set α) :
+  is_pi_system {S | ∃ (l ∈ s) (u ∈ t) (h : l < u), Ioo l u = S} :=
+is_pi_system_Ixx_mem (λ a b ⟨x, hax, hxb⟩, hax.trans hxb) (λ _ _ _ _, Ioo_inter_Ioo) s t
+
+lemma is_pi_system_Ioo (f : ι → α) (g : ι' → α) :
+  @is_pi_system α {S | ∃ l u (h : f l < g u), Ioo (f l) (g u) = S} :=
+is_pi_system_Ixx (λ a b ⟨x, hax, hxb⟩, hax.trans hxb) (λ _ _ _ _, Ioo_inter_Ioo) f g
+
+lemma is_pi_system_Ioc_mem (s t : set α) :
+  is_pi_system {S | ∃ (l ∈ s) (u ∈ t) (h : l < u), Ioc l u = S} :=
+is_pi_system_Ixx_mem (λ a b ⟨x, hax, hxb⟩, hax.trans_le hxb) (λ _ _ _ _, Ioc_inter_Ioc) s t
+
+lemma is_pi_system_Ioc (f : ι → α) (g : ι' → α) :
+  @is_pi_system α {S | ∃ i j (h : f i < g j), Ioc (f i) (g j) = S} :=
+is_pi_system_Ixx (λ a b ⟨x, hax, hxb⟩, hax.trans_le hxb) (λ _ _ _ _, Ioc_inter_Ioc) f g
+
+lemma is_pi_system_Ico_mem (s t : set α) :
+  is_pi_system {S | ∃ (l ∈ s) (u ∈ t) (h : l < u), Ico l u = S} :=
+is_pi_system_Ixx_mem (λ a b ⟨x, hax, hxb⟩, hax.trans_lt hxb) (λ _ _ _ _, Ico_inter_Ico) s t
+
+lemma is_pi_system_Ico (f : ι → α) (g : ι' → α) :
+  @is_pi_system α {S | ∃ i j (h : f i < g j), Ico (f i) (g j) = S} :=
+is_pi_system_Ixx (λ a b ⟨x, hax, hxb⟩, hax.trans_lt hxb) (λ _ _ _ _, Ico_inter_Ico) f g
+
+lemma is_pi_system_Icc_mem (s t : set α) :
+  is_pi_system {S | ∃ (l ∈ s) (u ∈ t) (h : l ≤ u), Icc l u = S} :=
+is_pi_system_Ixx_mem (λ a b, nonempty_Icc.1) (λ _ _ _ _, Icc_inter_Icc) s t
+
+lemma is_pi_system_Icc (f : ι → α) (g : ι' → α) :
+  @is_pi_system α {S | ∃ i j (h : f i ≤ g j), Icc (f i) (g j) = S} :=
+is_pi_system_Ixx (λ a b, nonempty_Icc.1) (λ _ _ _ _, Icc_inter_Icc) f g
+
+end order
+
 /-- Given a collection `S` of subsets of `α`, then `generate_pi_system S` is the smallest
 π-system containing `S`. -/
 inductive generate_pi_system {α} (S : set (set α)) : set (set α)

src/topology/algebra/ordered/basic.lean

@@ -95,10 +95,16 @@ instance : Π [topological_space α], topological_space (order_dual α) := id
 instance [topological_space α] [h : first_countable_topology α] :
   first_countable_topology (order_dual α) := h
 
+instance [topological_space α] [h : second_countable_topology α] :
+  second_countable_topology (order_dual α) := h
+
 @[to_additive]
 instance [topological_space α] [has_mul α] [h : has_continuous_mul α] :
   has_continuous_mul (order_dual α) := h
 
+lemma dense.order_dual [topological_space α] {s : set α} (hs : dense s) :
+  dense (order_dual.of_dual ⁻¹' s) := hs
+
 section order_closed_topology
 
 section preorder
@@ -520,6 +526,36 @@ lemma filter.tendsto.min {b : filter β} {a₁ a₂ : α} (hf : tendsto f b (
   tendsto (λb, min (f b) (g b)) b (𝓝 (min a₁ a₂)) :=
 (continuous_min.tendsto (a₁, a₂)).comp (hf.prod_mk_nhds hg)
 
+lemma dense.exists_lt [no_bot_order α] {s : set α} (hs : dense s) (x : α) : ∃ y ∈ s, y < x :=
+hs.exists_mem_open is_open_Iio (no_bot x)
+
+lemma dense.exists_gt [no_top_order α] {s : set α} (hs : dense s) (x : α) : ∃ y ∈ s, x < y :=
+hs.order_dual.exists_lt x
+
+lemma dense.exists_le [no_bot_order α] {s : set α} (hs : dense s) (x : α) : ∃ y ∈ s, y ≤ x :=
+(hs.exists_lt x).imp $ λ y hy, ⟨hy.fst, hy.snd.le⟩
+
+lemma dense.exists_ge [no_top_order α] {s : set α} (hs : dense s) (x : α) : ∃ y ∈ s, x ≤ y :=
+hs.order_dual.exists_le x
+
+lemma dense.exists_le' {s : set α} (hs : dense s) (hbot : ∀ x, is_bot x → x ∈ s) (x : α) :
+  ∃ y ∈ s, y ≤ x :=
+begin
+  by_cases hx : is_bot x,
+  { exact ⟨x, hbot x hx, le_rfl⟩ },
+  { simp only [is_bot, not_forall, not_le] at hx,
+    rcases hs.exists_mem_open is_open_Iio hx with ⟨y, hys, hy : y < x⟩,
+    exact ⟨y, hys, hy.le⟩ }
+end
+
+lemma dense.exists_ge' {s : set α} (hs : dense s) (htop : ∀ x, is_top x → x ∈ s) (x : α) :
+  ∃ y ∈ s, x ≤ y :=
+hs.order_dual.exists_le' htop x
+
+lemma dense.exists_between [densely_ordered α] {s : set α} (hs : dense s) {x y : α} (h : x < y) :
+  ∃ z ∈ s, z ∈ Ioo x y :=
+hs.exists_mem_open is_open_Ioo (nonempty_Ioo.2 h)
+
 end linear_order
 
 end order_closed_topology

src/topology/bases.lean

@@ -414,6 +414,36 @@ let ⟨t, htc, htd⟩ := exists_countable_dense s
 in ⟨coe '' t, image_subset_iff.2 $ λ x _, mem_preimage.2 $ subtype.coe_prop _, htc.image coe,
   hs.dense_range_coe.dense_image continuous_subtype_val htd⟩
 
+/-- Let `s` be a dense set in a topological space `α` with partial order structure. If `s` is a
+separable space (e.g., if `α` has a second countable topology), then there exists a countable
+dense subset `t ⊆ s` such that `t` contains bottom/top element of `α` when they exist and belong
+to `s`. -/
+lemma dense.exists_countable_dense_subset_bot_top {α : Type*} [topological_space α]
+  [partial_order α] {s : set α} [separable_space s] (hs : dense s) :
+  ∃ t ⊆ s, countable t ∧ dense t ∧ (∀ x, is_bot x → x ∈ s → x ∈ t) ∧
+    (∀ x, is_top x → x ∈ s → x ∈ t) :=
+begin
+  rcases hs.exists_countable_dense_subset with ⟨t, hts, htc, htd⟩,
+  refine ⟨(t ∪ ({x | is_bot x} ∪ {x | is_top x})) ∩ s, _, _, _, _, _⟩,
+  exacts [inter_subset_right _ _,
+    (htc.union ((countable_is_bot α).union (countable_is_top α))).mono (inter_subset_left _ _),
+    htd.mono (subset_inter (subset_union_left _ _) hts),
+    λ x hx hxs, ⟨or.inr $ or.inl hx, hxs⟩, λ x hx hxs, ⟨or.inr $ or.inr hx, hxs⟩]
+end
+
+instance separable_space_univ {α : Type*} [topological_space α] [separable_space α] :
+  separable_space (univ : set α) :=
+(equiv.set.univ α).symm.surjective.dense_range.separable_space
+  (continuous_subtype_mk _ continuous_id)
+
+/-- If `α` is a separable topological space with a partial order, then there exists a countable
+dense set `s : set α` that contains those of both bottom and top elements of `α` that actually
+exist. -/
+lemma exists_countable_dense_bot_top (α : Type*) [topological_space α] [separable_space α]
+  [partial_order α] :
+  ∃ s : set α, countable s ∧ dense s ∧ (∀ x, is_bot x → x ∈ s) ∧ (∀ x, is_top x → x ∈ s) :=
+by simpa using dense_univ.exists_countable_dense_subset_bot_top
+
 namespace topological_space
 universe u
 variables (α : Type u) [t : topological_space α]