FormalConjecturesForMathlib/Data/Finset/Powerset.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

4 declarations, 0 contain sorry, 0 declared as axioms

Imports (1)
Imported by 1 file
  1. lemma Finset.powersetCard_inter line 27 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: DecidableEq, Finset, Nat, Eq, Finset.powersetCard, Inter.inter

    Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, LE.le, Finset.card, id, congr, congrArg, Eq.trans, congrFun', and_and_right

    12 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  2. lemma Finset.disjoint_powersetCard_powersetCard line 30 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: DecidableEq, Finset, Nat, Iff, Disjoint, Finset.powersetCard, LT.lt, Finset.card, Inter.inter

    Proof uses: of_eq_true, Eq.trans, True, congrFun', congrArg, Eq, EmptyCollection.emptyCollection, iff_self

    13 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

    Open to load the checked before-and-after goal states.

  3. lemma Finset.filter_subset_powersetCard_card_add_one The (#t + 1)-subsets of s that contain t ⊆ s are exactly the sets insert a t with a ∈ s \ t line 36 source

    Source documentation

    The (#t + 1)-subsets of s that contain t ⊆ s are exactly the sets insert a t with a ∈ s \ t.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: DecidableEq, Finset, LE.le, Eq, Finset.filter, Finset.powersetCard, HAdd.hAdd, Nat, Finset.card, OfNat.ofNat, Finset.image, Insert.insert, SDiff.sdiff

    Proof uses: Finset.ext, Eq.mpr, Iff, Membership.mem, And, Exists, Not, id, congr, congrArg, Eq.trans, congrFun', funext, Iff.intro, HSub.hSub, Finset.card_sdiff_of_subset, Decidable.byContradiction, Singleton.singleton, Iff.mp, Finset.card_eq_one and 16 more

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 18 steps

    Open to load the checked before-and-after goal states.

    lemma filter_subset_powersetCard_card_add_one (h : t ⊆ s) :
    (powersetCard (#t + 1) s).filter (t ⊆ ·) = (s \ t).image (insert · t) := by
…
  4. lemma Finset.card_filter_subset_powersetCard_card_add_one A k-subset t of s lies in exactly #s - k of the (k + 1)-subsets of s line 52 source

    Source documentation

    A k-subset t of s lies in exactly #s - k of the (k + 1)-subsets of s.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: DecidableEq, Finset, LE.le, Eq, Nat, Finset.card, Finset.filter, Finset.powersetCard, HAdd.hAdd, OfNat.ofNat, HSub.hSub

    Proof uses: Eq.mpr, Finset.image, Insert.insert, SDiff.sdiff, id, congrArg, Finset.filter_subset_powersetCard_card_add_one, Finset.card_image_of_injOn, Membership.mem, Set, Eq.symm, Finset.mem_insert_self, Or.resolve_right, Eq.mp, Or, propext, Finset.mem_insert, And.right, Not, Iff.mp and 4 more

    25 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

    lemma card_filter_subset_powersetCard_card_add_one (h : t ⊆ s) :
    #((powersetCard (#t + 1) s).filter (t ⊆ ·)) = #s - #t := by
…