English
Characterization of open sets in a product, via finite index families of open sets.
Русский
Характеризация открытости в произведении через конечные семейства открытых множеств.
LaTeX
$$$\\displaystyle \\text{IsOpen}(s) \\iff \\forall f\\in s, \\exists I, u, \\text{(conditions involving } I, u) \\land I.\\pi u \\subseteq s.$$$
Lean4
theorem isOpen_pi_iff {s : Set (∀ a, A a)} :
IsOpen s ↔
∀ f,
f ∈ s → ∃ (I : Finset ι) (u : ∀ a, Set (A a)), (∀ a, a ∈ I → IsOpen (u a) ∧ f a ∈ u a) ∧ (I : Set ι).pi u ⊆ s :=
by
rw [isOpen_iff_nhds]
simp_rw [le_principal_iff, nhds_pi, Filter.mem_pi', mem_nhds_iff]
refine forall₂_congr fun a _ => ⟨?_, ?_⟩
· rintro ⟨I, t, ⟨h1, h2⟩⟩
refine ⟨I, fun a => eval a '' (I : Set ι).pi fun a => (h1 a).choose, fun i hi => ?_, ?_⟩
· simp_rw [eval_image_pi (Finset.mem_coe.mpr hi)
(pi_nonempty_iff.mpr fun i => ⟨_, fun _ => (h1 i).choose_spec.2.2⟩)]
exact (h1 i).choose_spec.2
· exact Subset.trans (pi_mono fun i hi => (eval_image_pi_subset hi).trans (h1 i).choose_spec.1) h2
· rintro ⟨I, t, ⟨h1, h2⟩⟩
classical
refine ⟨I, fun a => ite (a ∈ I) (t a) univ, fun i => ?_, ?_⟩
· by_cases hi : i ∈ I
· use t i
simp_rw [if_pos hi]
exact ⟨Subset.rfl, (h1 i) hi⟩
· use univ
simp_rw [if_neg hi]
exact ⟨Subset.rfl, isOpen_univ, mem_univ _⟩
· rw [← univ_pi_ite]
simp only [← ite_and, ← Finset.mem_coe, and_self_iff, univ_pi_ite, h2]
