powerset — Mathlib

English

Variant stating that if g ≤ f, then s.piecewise f g ∈ Icc g f.

Русский

Вариант: при g ≤ f, s.piecewise f g ∈ Icc g f.

LaTeX

$$$$ (h : g \\le f) : s.piecewise f g \\in \\mathrm{Icc}\\ g\\ f.$$$$

Lean4

/-- When `s` is a finset, `s.powerset` is the finset of all subsets of `s` (seen as finsets). -/
def powerset (s : Finset α) : Finset (Finset α) :=
  ⟨(s.1.powerset.pmap Finset.mk) fun _t h => nodup_of_le (mem_powerset.1 h) s.nodup,
    s.nodup.powerset.pmap fun _a _ha _b _hb => congr_arg Finset.val⟩

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