filter_subset_filter

Mathlib.Data.Finset.Filter

URI: https://scilib.ai/kg/mathlib#Finset.filter_subset_filter

← MathLib Explorer

English

If s ⊆ t, then s.filter p ⊆ t.filter p.

Русский

Если s ⊆ t, то s.filter p ⊆ t.filter p.

LaTeX

$$$s \\subseteq t \\Rightarrow s.filter p \\subseteq t.filter p$$$

Lean4

@[gcongr]
theorem filter_subset_filter {s t : Finset α} (h : s ⊆ t) : s.filter p ⊆ t.filter p := fun _a ha =>
  mem_filter.2 ⟨h (mem_filter.1 ha).1, (mem_filter.1 ha).2⟩

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

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

Разделы

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

Аффилиация

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