union_right_iff — Mathlib

English

AreSeparated(s, t ∪ t') holds iff AreSeparated(s,t) and AreSeparated(s,t').

Русский

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

LaTeX

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

Lean4

@[simp]
theorem union_right_iff {t'} : AreSeparated s (t ∪ t') ↔ AreSeparated s t ∧ AreSeparated s t' :=
  comm.trans <| union_left_iff.trans <| and_congr comm comm

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