Theorems · Theorem · general topology

IsClosed.relImage_of_finite

∀ {α : Type ua} {β : Type ub} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : SetRel α β},
  IsClosed s → ∀ {t : Set α}, t.Finite → IsClosed (s.image t)

Defined in

Mathlib.Topology.UniformSpace.Basic

Cited by

1 results in Mathlib

Foundations

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

Assumes

TopologicalSpaceTopologicalSpace