instNonemptyMap

Mathlib.Combinatorics.Matroid.Map

URI: https://scilib.ai/kg/mathlib#Matroid.instNonemptyMap

English

If M is nonempty, then its image under any map is nonempty.

Русский

Если исходный матроид непуст, то образ его отображения тоже непуст.

LaTeX

$$$ M.Nonempty \Rightarrow (M.map f hf).Nonempty $$$

Lean4

instance [M.Nonempty] {f : α → β} (hf) : (M.map f hf).Nonempty :=
  ⟨by simp [M.ground_nonempty]⟩

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

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

Разделы

Аффилиация

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