ne_key

Mathlib.Data.List.Sigma

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

English

a ∉ l.keys iff ∀ s ∈ l, s.1 ≠ a.

Русский

a не является ключом l, тогда и только тогда, когда для каждого s ∈ l, s.1 ≠ a.

LaTeX

$$$ a \\notin l.keys \\iff \\forall s \\in l, s.1 \\neq a. $$$

Lean4

theorem ne_key {a} {l : List (Sigma β)} : a ∉ l.keys ↔ ∀ s : Sigma β, s ∈ l → a ≠ s.1 := by grind

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

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

Разделы

Аффилиация

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