mem_ssubsets

Mathlib.Data.Finset.Powerset

URI: https://scilib.ai/kg/mathlib#Finset.mem_ssubsets

← MathLib Explorer

English

For any s,t, t is in s.ssubsets if and only if t is a proper subset of s.

Русский

Для любых s,t верно: t ∈ s.ssubsets тогда и только тогда, когда t ⊊ s.

LaTeX

$$t ∈ s.ssubsets ↔ t ⊂ s$$

Lean4

@[simp, grind =]
theorem mem_ssubsets {s t : Finset α} : t ∈ s.ssubsets ↔ t ⊂ s := by
  rw [ssubsets, mem_erase, mem_powerset, ssubset_iff_subset_ne, and_comm]

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

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

Разделы

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

Аффилиация

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