union_left_iff — Mathlib

English

AreSeparated(s ∪ s', t) holds if and only if AreSeparated(s,t) and AreSeparated(s',t).

Русский

AreSeparated(s ∪ s', t) эквивалентно AreSeparated(s,t) и AreSeparated(s',t).

LaTeX

$$$ \text{AreSeparated}(s \cup s', t) \iff (\text{AreSeparated}(s,t) \land \text{AreSeparated}(s',t)) $$$

Lean4

@[simp]
theorem union_left_iff {s'} : AreSeparated (s ∪ s') t ↔ AreSeparated s t ∧ AreSeparated s' t :=
  ⟨fun h => ⟨h.mono_left subset_union_left, h.mono_left subset_union_right⟩, fun h => h.1.union_left h.2⟩

Похожие утверждения