nonempty_finset

Mathlib.AlgebraicTopology.SimplicialObject.II

URI: https://scilib.ai/kg/mathlib#SimplexCategory.II.nonempty_finset

English

For any f and x, the finite set finset f x is nonempty, containing at least the last element.

Русский

Для любых f и x множество finset f x не пусто и содержит, как минимум, последний элемент.

LaTeX

$$$ (finset f x).Nonempty. $$$

Lean4

theorem nonempty_finset (f : Fin (n + 1) →o Fin (m + 1)) (x : Fin (m + 2)) : (finset f x).Nonempty :=
  ⟨Fin.last _, by simp [mem_finset_iff]⟩

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

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

Разделы

Аффилиация

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