interior of set pi

Stream: general

[Alex J. Best]

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]

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

[Louis Andrew Newton]

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

[Louis Andrew Newton]

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]

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

[Alex J. Best]

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

[Alex J. Best]

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]

I'll work on that.

[Alex J. Best]

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]

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]

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

[Patrick Massot]

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]

I'll open a PR later

[Eric Wieser]

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]

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]

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