Zulip Chat Archive

Stream: general

Topic: interior of set pi


Alex J. Best (Aug 11 2021 at 22:39):

Can any filter pro give a clean proof of the following (or is it already in mathlib?):
I just managed to prove that the interior of a finite product equals the product of the interiors, but it's possibly one of the ugliest Lean proofs I've ever written and I'm not sure I understand it to be quite honest.
P.S. I was surprised to note the forward direction interior (pi I s) ⊆ I.pi (λ i, interior (s i)) works even without the fintype assumption :hurt:

import topology.bases
open classical filter topological_space set

lemma interior_pi {ι : Type*} [fintype ι] {α : ι  Type*} [Π i, topological_space (α i)]
  {I : set ι} {s : Π i, set (α i)} :
  interior (pi I s) = I.pi (λ i, interior (s i)) :=
begin
  ext a,
  simp only [mem_pi, mem_interior_iff_mem_nhds],
  split,
  { intro h,
    rw (is_topological_basis_pi (λ i : ι, @is_topological_basis_opens (α i) _)).mem_nhds_iff at h,
    obtain t, U, F, htopen, rfl⟩, H₁, H₂ := h,
    intros i hi,
    rw mem_nhds_iff,
    dsimp only [subset_def, mem_pi] at H₂,
    classical,
    by_cases hiF : i  F,
    { use U i,
      rw mem_pi at H₁,
      refine _, htopen i hiF, H₁ i hiF⟩,
      intros x hx,
      have := H₂ (function.update a i x) _,
      { specialize this i hi,
        simpa, },
      { intros i' hi'F,
        rw function.update,
        split_ifs,
        { convert hx,
          exact eq_rec_heq h.symm x,},
        { exact H₁ _ hi'F, }, }, },
    { use univ,
      refine _, is_open_univ, mem_univ (a i)⟩,
      rw [univ_subset_iff, eq_univ_iff_forall],
      intro x,
      have := H₂ (function.update a i x) _,
      { specialize this i hi,
        simpa, },
      { intros i' hi'F,
        rw function.update,
        split_ifs,
        { rw h at hi'F,
          contradiction, },
        { exact H₁ _ hi'F, }, }, }, },
  { refine set_pi_mem_nhds (finite.of_fintype _), },
end

Eric Wieser (Aug 11 2021 at 23:05):

You shouldn't ever have to rw function.update, it has an API

Louis Andrew Newton (Aug 11 2021 at 23:54):

Hello! I am totally new here but excited to go down this rabbit hole!

Louis Andrew Newton (Aug 11 2021 at 23:57):

I have just watched this video on GPT-3 codex, and was wondering if the same approach could be used on the language of maths itself? Try and generate some Godel problem breaking AI :)

Louis Andrew Newton (Aug 11 2021 at 23:57):

https://www.youtube.com/watch?v=SGUCcjHTmGY

Alex J. Best (Aug 12 2021 at 09:42):

Yeah I agree but I couldn't find an api version of docs#function.update_apply for dependent functions.

Alex J. Best (Aug 12 2021 at 09:51):

Ok I made that part slightly neater by explicitly making the case split I want rather than rewriting function to use split ifs, but the principle is the same:

import topology.bases
open classical filter topological_space set

lemma interior_pi {ι : Type*} [fintype ι] {α : ι  Type*} [Π i, topological_space (α i)]
  {I : set ι} {s : Π i, set (α i)} :
  interior (pi I s) = I.pi (λ i, interior (s i)) :=
begin
  ext a,
  simp only [mem_pi, mem_interior_iff_mem_nhds],
  split,
  { intro h,
    rw (is_topological_basis_pi (λ i : ι, @is_topological_basis_opens (α i) _)).mem_nhds_iff at h,
    obtain t, U, F, htopen, rfl⟩, H₁, H₂ := h,
    intros i hi,
    rw mem_nhds_iff,
    dsimp only [subset_def, mem_pi] at H₂,
    classical,
    by_cases hiF : i  F,
    { use U i,
      rw mem_pi at H₁,
      refine _, htopen i hiF, H₁ i hiF⟩,
      intros x hx,
      simpa using H₂ (function.update a i x) _ i hi,
      intros i' hi'F,
      by_cases h : i = i',
      { subst h,
        rwa [function.update_same], },
      { rw function.update_noteq (ne.symm h),
        exact H₁ _ hi'F, }, },
    { use univ,
      refine _, is_open_univ, mem_univ (a i)⟩,
      rw [univ_subset_iff, eq_univ_iff_forall],
      intro x,
      simpa using H₂ (function.update a i x) _ i hi,
      intros i' hi'F,
      by_cases h : i = i',
      { subst h,
        contradiction, },
      { rw function.update_noteq (ne.symm h),
        exact H₁ _ hi'F, }, }, },
  { refine set_pi_mem_nhds (finite.of_fintype _), },
end

Patrick Massot (Aug 12 2021 at 10:40):

I'll work on that.

Alex J. Best (Aug 12 2021 at 10:42):

Nice, I made a PR at, https://github.com/leanprover-community/mathlib/pull/8642 feel free to push to that branch and overwrite the proof or just close it and make a new one if you find a better proof :smile:

Patrick Massot (Aug 12 2021 at 10:57):

I wrote the proof below, but it reminded me of very overdue stuff I needed to fix in order.filter.basis to make it a bit simpler.

import topology.constructions
open classical filter topological_space set function
open_locale topological_space

lemma Inter_ite {ι : Type*} {α : Type*} (f g : ι  set α) (I : set ι) [decidable_pred (λ x, x  I)]:
( i, if i  I then f i else g i) = ( i  I, f i)  ( i (h : i  I), g i) :=
begin
  ext x,
  simp,
  split,
  { intro h,
    split ;
    { intros i hi,
      simpa [hi] using h i } },
  { rintro h, h' i,
    split_ifs with hi,
    exacts [h i hi, h' i hi] }
end

lemma exists_Inter_of_mem_infi {ι : Type*} {α : Type*} {f : ι  filter α} {s}
  (hs : s   i, f i) :  t : ι  set α, ( i, t i  f i)  ( i, t i)  s  :=
begin
  classical,
  rcases mem_infi_iff'.mp hs with I, I_fin, V, hV, hV'⟩,
  refine λ i, if i  I then V i else univ, _, _⟩,
  { intro i,
    split_ifs,
    exacts [hV i h, univ_mem_sets] },
  { simp [Inter_ite, hV'] },
end

lemma image_projection_prod {ι : Type*} {α : ι  Type*} {v : Π (i : ι), set (α i)}
  (hv : (pi univ v).nonempty) (i : ι) :
  (λ (x : Π (i : ι), α i), x i) '' ( k, (λ (x : Π (j : ι), α j), x k) ⁻¹' v k) = v i:=
begin
  classical,
  apply subset.antisymm,
  { simp [Inter_subset] },
  { intros y y_in,
    simp only [mem_image, mem_Inter, mem_preimage],
    rcases hv with z, hz⟩,
    refine function.update z i y, _, update_same i y z⟩,
    rw @forall_update_iff ι α _ z i y (λ i t, t  v i),
    exact y_in, λ j hj, by simpa using hz j },
end

lemma pi_mem_nhds {ι : Type*} {α : ι  Type*} [Π (i : ι), topological_space (α i)]
  {I : set ι} {s : Π i, set (α i)} (a : Π i, α i) (hs : I.pi s  𝓝 a) {i : ι} (hi : i  I) :
  s i  𝓝 (a i) :=
begin
  set p := λ i, λ (x : Π (i : ι), α i), x i,
  rw [nhds_pi, pi_def] at hs,
  obtain t : ι  set (Π i, α i),
          ht :  i, t i  comap (p i) (𝓝 (a i)), ht' : ( (i : ι), t i)   i  I, p i ⁻¹' s i :=
    exists_Inter_of_mem_infi hs,
  simp only [exists_prop, mem_comap_sets] at ht,
  choose v hv hv' using ht,
  apply mem_sets_of_superset (hv i),
  have : ( i, p i ⁻¹' v i)  p i ⁻¹' s i,
    from ((Inter_subset_Inter hv').trans ht').trans (bInter_subset_of_mem hi),
  rwa [ image_subset_iff, image_projection_prod] at this,
  use a,
  rw [mem_univ_pi],
  exact λ j, mem_of_mem_nhds (hv j)
end

lemma pi_mem_nhds_iff {ι : Type*} [fintype ι] {α : ι  Type*} [Π (i : ι), topological_space (α i)]
  {I : set ι} {s : Π i, set (α i)} (a : Π i, α i) :
  I.pi s  𝓝 a   (i : ι), i  I  s i  𝓝 (a i) :=
by apply pi_mem_nhds, set_pi_mem_nhds $ finite.of_fintype I

lemma interior_pi {ι : Type*} [fintype ι] {α : ι  Type*} [Π i, topological_space (α i)]
  {I : set ι} {s : Π i, set (α i)} :
  interior (pi I s) = I.pi (λ i, interior (s i)) :=
by { ext a, simp only  [mem_pi, mem_interior_iff_mem_nhds, pi_mem_nhds_iff] }

Patrick Massot (Aug 12 2021 at 10:58):

Note that the goal was not to reduce the total number of lines, but to get the lemmas that should be there.

Patrick Massot (Aug 12 2021 at 11:02):

Note in particular how your function.update issue was not lack of API but Lean 3 being bad at unifying the motive in forall_update_iff

Patrick Massot (Aug 12 2021 at 11:04):

I'll open a PR later

Eric Wieser (Aug 12 2021 at 11:20):

I think it might make sense to write

(λ (x : Π (i : ι), α i), x i) '' ( k, (λ (x : Π (j : ι), α j), x k) ⁻¹' v k) = v i:=

as

(function.eval i) '' ( k, function.eval k ⁻¹' v k) = v i:=

(docs#function.eval)

Patrick Massot (Aug 12 2021 at 11:57):

I know this exists but in this context the name is really confusing. Here we really thing of it as a projection, not an evaluation.

Eric Wieser (Aug 12 2021 at 12:02):

That contention between eval and proj has come up elsewhere too; we have docs#pi.eval_add_monoid_hom but docs#linear_map.proj.


Last updated: Dec 20 2023 at 11:08 UTC