Theorems · Theorem · general topology

Metric.AreSeparated.finite_iUnion_right_iff

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

Defined in: Mathlib.Topology.MetricSpace.MetricSeparated
Cited by: 1 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.

Cites7

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 and proof · 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
Metric.AreSeparated.commproof · cited by 2

Cited by1

Results whose statement or proof uses this declaration.

Metric.AreSeparated.finset_iUnion_right_iffproof · cited by 1