kerase_keys_subset

Mathlib.Data.List.Sigma

URI: https://scilib.ai/kg/mathlib#List.kerase_keys_subset

English

(kerase a l).keys ⊆ l.keys.

Русский

(kerase a l).keys ⊆ l.keys.

LaTeX

$$$ (\kerase a l).keys \subseteq l.keys $$$

Lean4

theorem kerase_keys_subset (a) (l : List (Sigma β)) : (kerase a l).keys ⊆ l.keys :=
  ((kerase_sublist a l).map _).subset

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

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

Разделы

Аффилиация

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