Triplewise.lean`

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

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

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

14 declarations, 0 contain sorry, 0 declared as axioms

Imports (4)

Imported by 3 files

def Triplewise line 25 source
no axioms what this means
Proof uses: Ne
def Set.Triplewise The ternary relation r holds triplewise on the set s if r x y z for all distinct x y z ∈ s line 36 source
Source documentation
The ternary relation r holds triplewise on the set s if r x y z for all distinct x y z ∈ s.

no axioms what this means
Statement uses: Set
Proof uses: Membership.mem, Ne
1 instances, coercions and auxiliary constants left out.
```
protected def Triplewise (s : Set α) (r : α → α → α → Prop) : Prop :=
…
```
theorem Set.Triplewise.eq line 39 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Set.Triplewise, Membership.mem, Not, Or, Eq
Proof uses: Ne, False, Decidable.not_or_of_imp, Classical.propDecidable, Iff.mpr, Classical.or_iff_not_imp_left, False.elim, Decidable.of_not_not
4 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Set.Triplewise.mono line 45 source
no axioms what this means
Statement uses: Set, LE.le, Set.Triplewise
Proof uses: Membership.mem, Ne
3 instances, coercions and auxiliary constants left out.
theorem Set.Triplewise_univ_iff line 50 source
standard axioms: Quot.sound, propext what this means
Statement uses: Iff, Set.Triplewise, Set.univ, Triplewise
Proof uses: of_eq_true, Not, Eq, Eq.trans, True, congrFun', congrArg, forall_congr, Membership.mem, Set, implies_congr, Eq.refl, iff_self
5 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
theorem Set.triplewise_of_encard_lt line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, LT.lt, ENat, Set.encard, OfNat.ofNat, Nat, Set.Triplewise
Proof uses: id, Mathlib.Tactic.Contrapose.contrapose₁, Membership.mem, Ne, Eq.mpr, Not, Exists, And, LE.le, Eq, implies_congr, Eq.trans, Mathlib.Tactic.Push.not_forall_eq, congrArg, funext, Trans.simple, Insert.insert, Singleton.singleton, HAdd.hAdd, Set.encard_insert_of_notMem and 23 more
48 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.
theorem Set.triplewise_empty line 65 source
no axioms what this means
Statement uses: Set.Triplewise, EmptyCollection.emptyCollection, Set
Proof uses: Membership.mem, False.elim, Ne, Set.notMem_empty
3 instances, coercions and auxiliary constants left out.
theorem Set.triplewise_singleton line 70 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.Triplewise, Singleton.singleton, Set
Proof uses: Set.triplewise_of_encard_lt, of_eq_true, LT.lt, ENat, Set.encard, OfNat.ofNat, Nat, Eq.trans, True, congrFun', congrArg, Set.encard_singleton
26 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
theorem Set.triplewise_pair line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set.Triplewise, Insert.insert, Set, Singleton.singleton
Proof uses: Set.triplewise_of_encard_lt, LE.le.trans_lt, ENat, Set.encard, HAdd.hAdd, OfNat.ofNat, Nat, Set.encard_insert_le, Eq.mpr, LT.lt, id, Eq, congrFun', congrArg, Set.encard_singleton, Mathlib.Meta.NormNum.isNat_lt_true, Mathlib.Meta.NormNum.isNat_add, Eq.refl, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one and 3 more
29 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
theorem Set.triplewise_insert line 83 source
standard axioms: propext what this means
Statement uses: Set, Iff, Set.Triplewise, Insert.insert, And, Membership.mem, Ne
Proof uses: Iff.intro, And.intro, Set.Triplewise.mono, Set.subset_insert, Set.mem_insert, Set.mem_insert_of_mem, Ne.symm, Eq, Or, Eq.mp, congrArg, propext, Set.mem_insert_iff, And.left, Eq.trans, False, congrFun', eq_false, false_or, And.right
7 instances, coercions and auxiliary constants left out.

Tactic trace: 27 steps
Open to load the checked before-and-after goal states.
theorem Set.triplewise_insert_of_not_mem line 104 source
standard axioms: propext what this means
Statement uses: Set, Not, Membership.mem, Iff, Set.Triplewise, Insert.insert, And, Ne
Proof uses: Iff.trans, Set.triplewise_insert, and_congr_right', forall₄_congr, of_eq_true, Eq, Eq.trans, True, congrFun', congrArg, implies_congr, False, eq_false, Ne.symm, ne_of_mem_of_not_mem, not_false_eq_true, Eq.refl, iff_self
7 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
theorem Set.Triplewise.insert line 111 source
standard axioms: propext what this means
Statement uses: Set, Set.Triplewise, Membership.mem, Ne, And, Insert.insert
Proof uses: Iff.mpr, Set.triplewise_insert, And.intro
4 instances, coercions and auxiliary constants left out.
theorem Set.Triplewise.insert_of_not_mem line 116 source
standard axioms: propext what this means
Statement uses: Set, Not, Membership.mem, Set.Triplewise, Ne, And, Insert.insert
Proof uses: Iff.mpr, Set.triplewise_insert_of_not_mem, And.intro
4 instances, coercions and auxiliary constants left out.
theorem Set.triplewise_set_pred_iff line 122 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Set, Iff, Set.Triplewise, Insert.insert, Singleton.singleton, LE.le, Eq, Nat, Set.ncard, OfNat.ofNat
Proof uses: Iff.intro, Exists, And, Ne, Iff.mp, Set.ncard_eq_three, And.left, Membership.mem, Eq.mp, congrArg, Eq.trans, And.right, Eq.symm, of_eq_true, True, congr, eq_true, and_self, Iff.mpr, Exists.intro and 2 more
15 instances, coercions and auxiliary constants left out.

Tactic trace: 10 steps
Open to load the checked before-and-after goal states.