subset_ker

Mathlib.Order.Filter.Ker

URI: https://scilib.ai/kg/mathlib#Filter.subset_ker

English

A set s is contained in the kernel of f exactly when s is contained in every member of f.

Русский

Множество s содержится в ядре фильтра f тогда и только тогда, когда s ⊆ t для каждого t ∈ f.

LaTeX

$$$s \\subseteq f.ker \\iff \\forall t \\in f, s \\subseteq t$$$

Lean4

@[simp]
theorem subset_ker : s ⊆ f.ker ↔ ∀ t ∈ f, s ⊆ t :=
  subset_sInter_iff

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

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

Разделы

Аффилиация

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