English
If ι is countable and each t(i) is a second-countable topology on α, then the infimum topology ⨅ i, t(i) is second-countable.
Русский
Если индекс ι счетный и каждый t(i) задаёт вторую счетность на α, то инфимум топологий ⨅ i, t(i) тоже счетен.
LaTeX
$$$\forall t:\, ι \to TopologicalSpace(\alpha),\; Countable(ι) \land \forall i, SecondCountableTopology(\alpha, t(i)) \Rightarrow SecondCountableTopology(\alpha, \bigwedge_i t(i))$$$
Lean4
theorem secondCountableTopology_iInf {α ι} [Countable ι] {t : ι → TopologicalSpace α}
(ht : ∀ i, @SecondCountableTopology α (t i)) : @SecondCountableTopology α (⨅ i, t i) :=
by
rw [funext fun i => @eq_generateFrom_countableBasis α (t i) (ht i), ← generateFrom_iUnion]
exact
SecondCountableTopology.mk' <|
countable_iUnion fun i =>
@countable_countableBasis _ (t i)
(ht i)
-- TODO: more fine grained instances for `FirstCountableTopology`, `SeparableSpace`, `T2Space`, ...
