mem_keys_of_mem_keys_kerase

Mathlib.Data.List.Sigma

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

English

If a1 is in (kerase a2 l).keys, then a1 is in l.keys.

Русский

Если a1 принадлежит (kerase a2 l).keys, то a1 принадлежит l.keys.

LaTeX

$$$ a_1 \in (\kerase a_2 l).keys \Rightarrow a_1 \in l.keys $$$

Lean4

theorem mem_keys_of_mem_keys_kerase {a₁ a₂} {l : List (Sigma β)} : a₁ ∈ (kerase a₂ l).keys → a₁ ∈ l.keys :=
  @kerase_keys_subset _ _ _ _ _ _

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

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

Разделы

Аффилиация

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