any_of_mem

Mathlib.Data.Bool.AllAny

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

English

If a ∈ l and p(a) holds, then there exists some x ∈ l such that p(x) holds.

Русский

Если a ∈ l и p(a) выполняется, то существует элемент x ∈ l такой, что p(x) выполняется.

LaTeX

$$$$ a \in l \land p(a) \Rightarrow \exists x \in l,\ p(x). $$$$

Lean4

theorem any_of_mem {p : α → Bool} (h₁ : a ∈ l) (h₂ : p a) : any l p :=
  any_eq_true.2 ⟨_, h₁, h₂⟩

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

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

Разделы

Аффилиация

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