isSeparable_pi — Mathlib

English

A specialization of isSeparable_univ_pi for a pi-type.

Русский

Спецификация isSeparable_pi для типа пи.

LaTeX

$$$IsSeparable\ s \rightarrow IsSeparable( Set.univ.pi t )$$$

Lean4

theorem isSeparable_pi {ι : Type*} [Countable ι] {α : ι → Type*} {s : ∀ i, Set (α i)} [∀ i, TopologicalSpace (α i)]
    (h : ∀ i, IsSeparable (s i)) : IsSeparable {f : ∀ i, α i | ∀ i, f i ∈ s i} := by
  simpa only [← mem_univ_pi] using IsSeparable.univ_pi h

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