mem_powerset — Mathlib

English

For Finset powerset, membership characterizes as subset containment: s ∈ powerset t iff s ⊆ t.

Русский

Для множества подмножеств Finset: s ∈ powerset t эквивалентно s ⊆ t.

LaTeX

$$$$ s \\in \\text{powerset}(t) \\;\\Longleftrightarrow\\; s \\subseteq t. $$$$

Lean4

@[simp, grind =]
theorem mem_powerset {s t : Finset α} : s ∈ powerset t ↔ s ⊆ t :=
  by
  cases s
  simp [powerset, mem_mk, mem_pmap, mk.injEq, exists_prop, exists_eq_right, ← val_le_iff]

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