forall_const

Mathlib.Data.Finset.Empty

URI: https://scilib.ai/kg/mathlib#Finset.Nonempty.forall_const

English

If s is nonempty, then (for all x in s, p) is equivalent to p.

Русский

Если s непусто, то (для всех x ∈ s, p) эквивалентно p.

LaTeX

$$$s \\\\neq \\\\emptyset \\\\Rightarrow \\\\bigl( \\\$\\\\forall x \\\\in s, p\\\$ \\\\bigr) \\\\iff p$$$

Lean4

theorem forall_const {s : Finset α} (h : s.Nonempty) {p : Prop} : (∀ x ∈ s, p) ↔ p :=
  let ⟨x, hx⟩ := h
  ⟨fun h => h x hx, fun h _ _ => h⟩

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

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

Разделы

Аффилиация

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