notMem_of_prop_diff_singleton

Mathlib.Order.Minimal

URI: https://scilib.ai/kg/mathlib#Minimal.notMem_of_prop_diff_singleton

← MathLib Explorer

English

If h: Minimal P s and hx: P (s \\ { x }), then x ∉ s.

Русский

Если h: Minimal P s и hx: P (s \\ { x }), то x ∉ s.

LaTeX

$$$$ (h : Minimal P s) \\land (hx : P (s \\ { x })) \\Rightarrow x \\notin s. $$$$

Lean4

theorem notMem_of_prop_diff_singleton (h : Minimal P s) (hx : P (s \ { x })) : x ∉ s := fun hxs ↦
  ((h.eq_of_superset hx diff_subset).subset hxs).2 rfl

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

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

Разделы

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

Аффилиация

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