isOpen_pi_iff' — Mathlib

English

A finite-index variant of the open-set criterion for Pi-types using decidable predicates.

Русский

Конечнозначная версия критерия открытости для Pi-типов через разрешимые предикаты.

LaTeX

$$$\\displaystyle \\text{isOpen_pi_iff'} \text{ (finite ι) }$$$

Lean4

theorem isOpen_pi_iff' [Finite ι] {s : Set (∀ a, A a)} :
    IsOpen s ↔ ∀ f, f ∈ s → ∃ u : ∀ a, Set (A a), (∀ a, IsOpen (u a) ∧ f a ∈ u a) ∧ univ.pi u ⊆ s :=
  by
  cases nonempty_fintype ι
  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
      ⟨fun i => (h1 i).choose,
        ⟨fun i => (h1 i).choose_spec.2, (pi_mono fun i _ => (h1 i).choose_spec.1).trans (Subset.trans ?_ h2)⟩⟩
    rw [← pi_inter_compl (I : Set ι)]
    exact inter_subset_left
  · exact fun ⟨u, ⟨h1, _⟩⟩ => ⟨Finset.univ, u, ⟨fun i => ⟨u i, ⟨rfl.subset, h1 i⟩⟩, by rwa [Finset.coe_univ]⟩⟩

Похожие утверждения