subset_iUnion_of_subset

Mathlib.Data.Set.Lattice

URI: https://scilib.ai/kg/mathlib#Set.subset_iUnion_of_subset

← MathLib Explorer

English

If s ⊆ t_i for some i, then s ⊆ ⋃_i t_i.

Русский

Если s ⊆ t_i для некоторого i, тогда s ⊆ ⋃_i t_i.

LaTeX

$$$(s \subseteq t_i) \Rightarrow s \subseteq \bigcup_i t_i$$$

Lean4

/-- This rather trivial consequence of `subset_iUnion`is convenient with `apply`, and has `i`
explicit for this purpose. -/
theorem subset_iUnion_of_subset {s : Set α} {t : ι → Set α} (i : ι) (h : s ⊆ t i) : s ⊆ ⋃ i, t i :=
  le_iSup_of_le i h

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru