Theorems · Theorem · general topology

Set.Finite.isClopen_biInter

∀ {X : Type u} [inst : TopologicalSpace X] {Y : Type u_2} {s : Set Y},
  s.Finite → ∀ {f : Y → Set X}, (∀ i ∈ s, IsClopen (f i)) → IsClopen (⋂ i ∈ s, f i)

Defined in

Mathlib.Topology.Clopen

Cited by

1 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

TopologicalSpace