inter

Mathlib.Topology.GDelta.Basic

URI: https://scilib.ai/kg/mathlib#IsGδ.inter

English

The intersection of two Gδ sets is a Gδ set.

Русский

Пересечение двух Gδ множеств является Gδ.

LaTeX

$$$IsGδ(s) \\land IsGδ(t) \\Rightarrow IsGδ(s \\cap t)$$$

Lean4

theorem inter {s t : Set X} (hs : IsGδ s) (ht : IsGδ t) : IsGδ (s ∩ t) :=
  by
  rw [inter_eq_iInter]
  exact .iInter (Bool.forall_bool.2 ⟨ht, hs⟩)

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru