union_left — Mathlib

English

If s is separated from t and s' is separated from t, then s ∪ s' is separated from t.

Русский

Если S отделено от T и S' отделено от T, тогда S ∪ S' отделено от T.

LaTeX

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

Lean4

theorem union_left {s'} (h : AreSeparated s t) (h' : AreSeparated s' t) : AreSeparated (s ∪ s') t :=
  by
  rcases h, h' with ⟨⟨r, r0, hr⟩, ⟨r', r0', hr'⟩⟩
  refine ⟨min r r', ?_, fun x hx y hy => hx.elim ?_ ?_⟩
  · rw [← pos_iff_ne_zero] at r0 r0' ⊢
    exact lt_min r0 r0'
  · exact fun hx => (min_le_left _ _).trans (hr _ hx _ hy)
  · exact fun hx => (min_le_right _ _).trans (hr' _ hx _ hy)

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