mem_powersetCardAux — Mathlib

English

s ∈ powersetCardAux n l iff s ≤ ↑l and card s = n.

Русский

s ∈ powersetCardAux n l тогда и только тогда, когда s ≤ ↑l и card s = n.

LaTeX

$$s ∈ \\mathrm{powersetCardAux}(n,l) \\iff (s \\le \\uparrow l) \\land \\mathrm{card}(s) = n$$

Lean4

@[simp]
theorem mem_powersetCardAux {n} {l : List α} {s} : s ∈ powersetCardAux n l ↔ s ≤ ↑l ∧ card s = n :=
  Quotient.inductionOn s <|
    by
    simp only [quot_mk_to_coe, powersetCardAux_eq_map_coe, List.mem_map, mem_sublistsLen, coe_eq_coe, coe_le, Subperm,
      coe_card]
    exact fun l₁ =>
      ⟨fun ⟨l₂, ⟨s, e⟩, p⟩ => ⟨⟨_, p, s⟩, p.symm.length_eq.trans e⟩, fun ⟨⟨l₂, p, s⟩, e⟩ =>
        ⟨_, ⟨s, p.length_eq.trans e⟩, p⟩⟩

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