superset — Mathlib

English

Let s and t be subsets of a type α endowed with a Bornology. If s is cobounded and s ⊆ t, then t is cobounded as well.

Русский

Пусть α обладает борологией. Пусть s и t — подмножества α. Если s кобондировано и s ⊆ t, то и t кобондировано.

LaTeX

$$$\text{IsCobounded}(s) \rightarrow (s \subseteq t) \rightarrow \text{IsCobounded}(t)$$$

Lean4

theorem superset (hs : IsCobounded s) (ht : s ⊆ t) : IsCobounded t :=
  mem_of_superset hs ht

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