mono — Mathlib

English

Let s, t, s', t' be subsets of a metric-type space with s ⊆ s' and t ⊆ t'. If s' is separated from t', then s is separated from t.

Русский

Пусть S, T, S', T' – подмножества множества X с неравенствами S ⊆ S' и T ⊆ T'. Если S' отделено от T', то S отделено от T.

LaTeX

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

Lean4

@[mono]
theorem mono {s' t'} (hs : s ⊆ s') (ht : t ⊆ t') : AreSeparated s' t' → AreSeparated s t := fun ⟨r, r0, hr⟩ =>
  ⟨r, r0, fun x hx y hy => hr x (hs hx) y (ht hy)⟩

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