find_mem

Mathlib.Topology.ShrinkingLemma

URI: https://scilib.ai/kg/mathlib#ShrinkingLemma.PartialRefinement.find_mem

← MathLib Explorer

English

Given a nonempty chain, the element a chosen by find lies in the chain.

Русский

Для непустой цепи элемент, возвращаемый find, принадлежит цепи.

LaTeX

$$v ∈ c ∧ ne.some_mem → find c ne i ∈ c$$

Lean4

theorem find_mem {c : Set (PartialRefinement u s p)} (i : ι) (ne : c.Nonempty) : find c ne i ∈ c :=
  by
  rw [find]
  split_ifs with h
  exacts [h.choose_spec.1, ne.some_mem]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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