mono — Mathlib

English

If there exists a separating cover for (s2,t2) and s1 ⊆ s2, t1 ⊆ t2, then there exists 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 {s₁ s₂ t₁ t₂ : Set X} (sc_st : HasSeparatingCover s₂ t₂) (s_sub : s₁ ⊆ s₂) (t_sub : t₁ ⊆ t₂) :
    HasSeparatingCover s₁ t₁ := by
  obtain ⟨u, u_cov, u_props⟩ := sc_st
  exact ⟨u, s_sub.trans u_cov, fun n ↦ ⟨(u_props n).1, disjoint_of_subset (fun ⦃_⦄ a ↦ a) t_sub (u_props n).2⟩⟩

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