some_mem_insertBot

Mathlib.Order.Interval.Finset.Defs

URI: https://scilib.ai/kg/mathlib#WithBot.some_mem_insertBot

English

The membership of WithBot.insertBot s respects the membership of s via the some embedding.

Русский

Принадлежность элементы в insertBot сохраняется через отображение some.

LaTeX

$$$ \text{some\_mem\_insertBot} : \forall s,a, \; a \in insertBot(s) \iff a \in s $$$

Lean4

@[simp]
theorem some_mem_insertBot {s : Finset α} {a : α} : ↑a ∈ insertBot s ↔ a ∈ s := by simp [insertBot]

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

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

Разделы

Аффилиация

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