exists_mem

Mathlib.Order.Zorn

URI: https://scilib.ai/kg/mathlib#Flag.exists_mem

English

For every element a, there exists a flag s containing a.

Русский

Для каждого элемента a существует флаг s, содержащий a.

LaTeX

$$$\forall a,\exists s : Flag\; α,\ a \in s.$$$

Lean4

theorem exists_mem (a : α) : ∃ s : Flag α, a ∈ s :=
  let ⟨s, hs⟩ := Set.subsingleton_singleton (a := a).isChain.exists_subset_flag
  ⟨s, hs rfl⟩

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

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

Разделы

Аффилиация

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