subset — Mathlib

English

If s1 ⊆ s2 and s2 is totally bounded, then s1 is totally bounded.

Русский

Если s1 ⊆ s2 и s2 полностью ограничено, тогда s1 тоже полностью ограничено.

LaTeX

$$$$s_1 \\subseteq s_2 \\land TotallyBounded(s_2) \\Rightarrow TotallyBounded(s_1).$$$$

Lean4

theorem subset {s₁ s₂ : Set α} (hs : s₁ ⊆ s₂) (h : TotallyBounded s₂) : TotallyBounded s₁ := fun d hd =>
  let ⟨t, ht₁, ht₂⟩ := h d hd
  ⟨t, ht₁, Subset.trans hs ht₂⟩

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