Theorems · Theorem · general topology

Metric.AreSeparated.union_left_iff

∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t s' : Set X},
  Metric.AreSeparated (s ∪ s') t ↔ Metric.AreSeparated s t ∧ Metric.AreSeparated s' t

Defined in: Mathlib.Topology.MetricSpace.MetricSeparated
Cited by: 2 results in Mathlib
Foundations: Depth 151 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
PseudoEMetricSpacestatement and proof · cited by 1,536
Set.subset_union_leftproof · cited by 142
Set.subset_union_rightproof · cited by 123
Metric.AreSeparatedstatement and proof · cited by 23
Metric.AreSeparated.union_leftproof · cited by 2
Metric.AreSeparated.mono_leftproof · cited by 1

Cited by2

Results whose statement or proof uses this declaration.

Metric.AreSeparated.finite_iUnion_left_iffproof · cited by 3
Metric.AreSeparated.union_right_iffproof · cited by 0