Theorems · Theorem · general topology

Metric.AreSeparated.finite_iUnion_left

∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {ι : Type u_3} {I : Set ι},
  I.Finite →
    ∀ {s : ι → Set X} {t : Set X}, (∀ i ∈ I, Metric.AreSeparated (s i) t) → Metric.AreSeparated (⋃ i ∈ I, s i) t

Alias of the reverse direction of Metric.AreSeparated.finite_iUnion_left_iff.

Defined in: Mathlib.Topology.MetricSpace.MetricSeparated
Cited by: 0 results in Mathlib
Foundations: Depth 153 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: PseudoEMetricSpace

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites6

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Setstatement and proof · cited by 53,352
Set.iUnionstatement · cited by 2,483
Set.Finitestatement and proof · cited by 1,814
PseudoEMetricSpacestatement and proof · cited by 1,536
Metric.AreSeparatedstatement · cited by 23
Metric.AreSeparated.finite_iUnion_left_iffproof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.