mono — Mathlib

English

If there is a separating cover for s2,t2 and s1 ⊆ s2 and t1 ⊆ t2, then there is a separating cover for s1,t1.

Русский

Если существует разделяющее покрытие для s2,t2 и s1 ⊆ s2, t1 ⊆ t2, то существует разделяющее покрытие для s1,t1.

LaTeX

$$$ \mathrm{HasSeparatingCover}(s_2,t_2) \to s_1 \subseteq s_2 \to t_1 \subseteq t_2 \to \mathrm{HasSeparatingCover}(s_1,t_1) $$$

Lean4

theorem mono (h : SeparatedNhds s₂ t₂) (hs : s₁ ⊆ s₂) (ht : t₁ ⊆ t₂) : SeparatedNhds s₁ t₁ :=
  let ⟨U, V, hU, hV, hsU, htV, hd⟩ := h
  ⟨U, V, hU, hV, hs.trans hsU, ht.trans htV, hd⟩

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