mem_of_prop_insert

Mathlib.Order.Minimal

URI: https://scilib.ai/kg/mathlib#Maximal.mem_of_prop_insert

English

If h: Maximal P s and hx: P (insert x s), then x ∈ s.

Русский

Если h: Maximal P s и hx: P (вставка x в s), тогда x ∈ s.

LaTeX

$$$$ (h : Maximal P s) \\land (hx : P (\\text{insert } x s)) \\Rightarrow x \\in s. $$$$

Lean4

theorem mem_of_prop_insert (h : Maximal P s) (hx : P (insert x s)) : x ∈ s :=
  h.eq_of_subset hx (subset_insert _ _) ▸ mem_insert ..

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

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

Разделы

Аффилиация

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