Subpolyads of a triadic polyad

A Subpolyad3 P selects arbitrary subgraphs of the three pair supports of P. Its triple support is computed by requiring all three coordinate pairs to be selected. These are the subtriad tests used in hypergraph regularity; restricting the three vertex cells is only a special case, supplied by Subpolyad3.ofSubcells.

Subpolyads are extensional in their three selected pair graphs and form a finite type, even without a finite pair palette. Their supports lie in the parent support. Nonempty finite intersections are formed coordinatewise and their supports are the intersections of the supports. The subcell constructor accepts arbitrary vertex sets and intersects with the parent pair supports, so no containment hypotheses are needed. Subpolyad3.unionSupport collects the supports of a finite family. A family of at most r members has the same union as one indexed by Fin r. When the pair graphs of a polyad P', possibly over another skeleton, lie in those of P, Subpolyad3.inclusion regards each subpolyad of P' as a subpolyad of P with the same support. For arbitrary polyads P and P', Subpolyad3.restrict intersects the selected pair graphs with those of P; the resulting support is the part of the original one lying in P.

References

• V. Rödl and M. Schacht, Regular partitions of hypergraphs: regularity lemmas.
• B. Nagle, V. Rödl and M. Schacht, The counting lemma for regular k-uniform hypergraphs.
• C. Terry, Growth of regular partitions 4: strong regularity and the pairs partition, arXiv:2404.02030.

structure TauCeti.Subpolyad3 {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) : Type u_2

A subpolyad selects arbitrary subgraphs of the three canonically oriented pair graphs of its parent. Its triple support is derived, not independently chosen.

• pair₀₁ : Finset { p : V × V // p.1 ≠ p.2 }

  The selected pairs on roles zero and one.

• pair₀₂ : Finset { p : V × V // p.1 ≠ p.2 }

  The selected pairs on roles zero and two.

• pair₁₂ : Finset { p : V × V // p.1 ≠ p.2 }

  The selected pairs on roles one and two.

• pair₀₁_sub : self.pair₀₁ ⊆ P.pairSupport₀₁

  The selected zero-one pairs belong to the parent pair graph.

• pair₀₂_sub : self.pair₀₂ ⊆ P.pairSupport₀₂

  The selected zero-two pairs belong to the parent pair graph.

• pair₁₂_sub : self.pair₁₂ ⊆ P.pairSupport₁₂

  The selected one-two pairs belong to the parent pair graph.

noncomputable def TauCeti.subpolyadSupport {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) (q₀₁ q₀₂ q₁₂ : Finset { p : V × V // p.1 ≠ p.2 }) : Finset { x : Fin 3 → V // Function.Injective x }

The parent triples whose three coordinate pairs lie in three prescribed pair sets.

@[simp]

theorem TauCeti.mem_subpolyadSupport {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {q₀₁ q₀₂ q₁₂ : Finset { p : V × V // p.1 ≠ p.2 }} {x : { x : Fin 3 → V // Function.Injective x }} : x ∈ subpolyadSupport P q₀₁ q₀₂ q₁₂ ↔ x ∈ P.support ∧ coordPair x 0 1 mem_subpolyadSupport._proof_1 ∈ q₀₁ ∧ coordPair x 0 2 mem_subpolyadSupport._proof_2 ∈ q₀₂ ∧ coordPair x 1 2 mem_subpolyadSupport._proof_3 ∈ q₁₂

Membership in a computed subpolyad support.

theorem TauCeti.Subpolyad3.ext_data {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {Q R : Subpolyad3 P} (h₀₁ : Q.pair₀₁ = R.pair₀₁) (h₀₂ : Q.pair₀₂ = R.pair₀₂) (h₁₂ : Q.pair₁₂ = R.pair₁₂) : Q = R

Two subpolyads agree precisely when their three selected pair graphs agree.

theorem TauCeti.Subpolyad3.ext_data_iff {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {Q R : Subpolyad3 P} : Q = R ↔ Q.pair₀₁ = R.pair₀₁ ∧ Q.pair₀₂ = R.pair₀₂ ∧ Q.pair₁₂ = R.pair₁₂

@[instance_reducible]

instance TauCeti.Subpolyad3.instDecidableEq {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} : DecidableEq (Subpolyad3 P)

Equality of subpolyads is decidable without a decidable pair palette.

@[instance_reducible]

noncomputable instance TauCeti.Subpolyad3.instFintype {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} : Fintype (Subpolyad3 P)

A finite host admits only finitely many subpolyads of any fixed polyad.

noncomputable def TauCeti.Subpolyad3.support {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} (Q : Subpolyad3 P) : Finset { x : Fin 3 → V // Function.Injective x }

The injective triples whose three coordinate pairs belong to the selected pair graphs.

theorem TauCeti.Subpolyad3.mem_support {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} (Q : Subpolyad3 P) (x : { x : Fin 3 → V // Function.Injective x }) : x ∈ Q.support ↔ x ∈ P.support ∧ coordPair x 0 1 mem_subpolyadSupport._proof_1 ∈ Q.pair₀₁ ∧ coordPair x 0 2 mem_subpolyadSupport._proof_2 ∈ Q.pair₀₂ ∧ coordPair x 1 2 mem_subpolyadSupport._proof_3 ∈ Q.pair₁₂

Membership in the support of a subpolyad.

theorem TauCeti.Subpolyad3.support_subset {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} (Q : Subpolyad3 P) : Q.support ⊆ P.support

A subpolyad's support lies in the parent support.

@[simp]

theorem TauCeti.Subpolyad3.mem_support_iff_coordPair_mem {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} (Q : Subpolyad3 P) (x : { x : Fin 3 → V // Function.Injective x }) : x ∈ Q.support ↔ coordPair x 0 1 mem_subpolyadSupport._proof_1 ∈ Q.pair₀₁ ∧ coordPair x 0 2 mem_subpolyadSupport._proof_2 ∈ Q.pair₀₂ ∧ coordPair x 1 2 mem_subpolyadSupport._proof_3 ∈ Q.pair₁₂

For a bundled subpolyad, membership in the three selected pair graphs already implies membership in the parent support.

theorem TauCeti.Subpolyad3.support_mono {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {Q R : Subpolyad3 P} (h₀₁ : Q.pair₀₁ ⊆ R.pair₀₁) (h₀₂ : Q.pair₀₂ ⊆ R.pair₀₂) (h₁₂ : Q.pair₁₂ ⊆ R.pair₁₂) : Q.support ⊆ R.support

Enlarging each selected pair graph can only enlarge the supported triples.

noncomputable def TauCeti.Subpolyad3.finsetInter {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} (s : Finset ι) (hs : s.Nonempty) (Q : ι → Subpolyad3 P) : Subpolyad3 P

The intersection of a nonempty finite family of subpolyads, formed by intersecting each of their three selected pair graphs.

@[simp]

theorem TauCeti.Subpolyad3.finsetInter_pair₀₁ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} (s : Finset ι) (hs : s.Nonempty) (Q : ι → Subpolyad3 P) : (finsetInter s hs Q).pair₀₁ = s.inf' hs fun (i : ι) => (Q i).pair₀₁

The zero-one pair graph of a finite intersection.

@[simp]

theorem TauCeti.Subpolyad3.finsetInter_pair₀₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} (s : Finset ι) (hs : s.Nonempty) (Q : ι → Subpolyad3 P) : (finsetInter s hs Q).pair₀₂ = s.inf' hs fun (i : ι) => (Q i).pair₀₂

The zero-two pair graph of a finite intersection.

@[simp]

theorem TauCeti.Subpolyad3.finsetInter_pair₁₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} (s : Finset ι) (hs : s.Nonempty) (Q : ι → Subpolyad3 P) : (finsetInter s hs Q).pair₁₂ = s.inf' hs fun (i : ι) => (Q i).pair₁₂

The one-two pair graph of a finite intersection.

@[simp]

theorem TauCeti.Subpolyad3.support_finsetInter {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} (s : Finset ι) (hs : s.Nonempty) (Q : ι → Subpolyad3 P) : (finsetInter s hs Q).support = s.inf' hs fun (i : ι) => (Q i).support

A finite intersection of subpolyads supports exactly the intersection of their supports.

noncomputable def TauCeti.Subpolyad3.ofSubcells {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) (a₀ a₁ a₂ : Finset V) : Subpolyad3 P

Restrict a polyad to three vertex sets, intersecting each parent pair graph with the corresponding vertex rectangle. The sets need not be contained in the parent cells.

@[simp]

theorem TauCeti.Subpolyad3.mem_ofSubcells_pair₀₁ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) (a₀ a₁ a₂ : Finset V) (p : { p : V × V // p.1 ≠ p.2 }) : p ∈ (ofSubcells P a₀ a₁ a₂).pair₀₁ ↔ p ∈ P.pairSupport₀₁ ∧ (↑p).1 ∈ a₀ ∧ (↑p).2 ∈ a₁

The selected zero-one pairs of a vertex restriction.

@[simp]

theorem TauCeti.Subpolyad3.mem_ofSubcells_pair₀₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) (a₀ a₁ a₂ : Finset V) (p : { p : V × V // p.1 ≠ p.2 }) : p ∈ (ofSubcells P a₀ a₁ a₂).pair₀₂ ↔ p ∈ P.pairSupport₀₂ ∧ (↑p).1 ∈ a₀ ∧ (↑p).2 ∈ a₂

The selected zero-two pairs of a vertex restriction.

@[simp]

theorem TauCeti.Subpolyad3.mem_ofSubcells_pair₁₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) (a₀ a₁ a₂ : Finset V) (p : { p : V × V // p.1 ≠ p.2 }) : p ∈ (ofSubcells P a₀ a₁ a₂).pair₁₂ ↔ p ∈ P.pairSupport₁₂ ∧ (↑p).1 ∈ a₁ ∧ (↑p).2 ∈ a₂

The selected one-two pairs of a vertex restriction.

@[simp]

theorem TauCeti.Subpolyad3.mem_ofSubcells_support {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) (a₀ a₁ a₂ : Finset V) (x : { x : Fin 3 → V // Function.Injective x }) : x ∈ (ofSubcells P a₀ a₁ a₂).support ↔ x ∈ P.support ∧ ↑x 0 ∈ a₀ ∧ ↑x 1 ∈ a₁ ∧ ↑x 2 ∈ a₂

A vertex restriction keeps exactly the parent triples landing in the three given sets.

theorem TauCeti.Subpolyad3.support_ofSubcells {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) (a₀ a₁ a₂ : Finset V) : (ofSubcells P a₀ a₁ a₂).support = {x ∈ P.support | ↑x 0 ∈ a₀ ∧ ↑x 1 ∈ a₁ ∧ ↑x 2 ∈ a₂}

The support of a vertex restriction, as a filter of the parent support.

@[simp]

theorem TauCeti.Subpolyad3.support_ofSubcells_cells {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} (P : Polyad3 S) : (ofSubcells P P.c₀ P.c₁ P.c₂).support = P.support

Restricting to the whole parent cells preserves the support, including repeated cells.

def TauCeti.Subpolyad3.inclusion {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {κ' : Type u_3} {S' : PairSkeleton3 κ' V} {P' : Polyad3 S'} (h₀₁ : P'.pairSupport₀₁ ⊆ P.pairSupport₀₁) (h₀₂ : P'.pairSupport₀₂ ⊆ P.pairSupport₀₂) (h₁₂ : P'.pairSupport₁₂ ⊆ P.pairSupport₁₂) (Q : Subpolyad3 P') : Subpolyad3 P

A subpolyad of P' regarded as a subpolyad of P, when each pair graph of P' lies in the corresponding pair graph of P. The polyad P' may live over a different skeleton, for instance one refining the skeleton of P. The selected pairs are unchanged.

@[simp]

theorem TauCeti.Subpolyad3.inclusion_pair₀₁ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {κ' : Type u_3} {S' : PairSkeleton3 κ' V} {P' : Polyad3 S'} (h₀₁ : P'.pairSupport₀₁ ⊆ P.pairSupport₀₁) (h₀₂ : P'.pairSupport₀₂ ⊆ P.pairSupport₀₂) (h₁₂ : P'.pairSupport₁₂ ⊆ P.pairSupport₁₂) (Q : Subpolyad3 P') : (inclusion h₀₁ h₀₂ h₁₂ Q).pair₀₁ = Q.pair₀₁

A subpolyad and its inclusion select the same pairs on roles zero and one.

@[simp]

theorem TauCeti.Subpolyad3.inclusion_pair₀₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {κ' : Type u_3} {S' : PairSkeleton3 κ' V} {P' : Polyad3 S'} (h₀₁ : P'.pairSupport₀₁ ⊆ P.pairSupport₀₁) (h₀₂ : P'.pairSupport₀₂ ⊆ P.pairSupport₀₂) (h₁₂ : P'.pairSupport₁₂ ⊆ P.pairSupport₁₂) (Q : Subpolyad3 P') : (inclusion h₀₁ h₀₂ h₁₂ Q).pair₀₂ = Q.pair₀₂

A subpolyad and its inclusion select the same pairs on roles zero and two.

@[simp]

theorem TauCeti.Subpolyad3.inclusion_pair₁₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {κ' : Type u_3} {S' : PairSkeleton3 κ' V} {P' : Polyad3 S'} (h₀₁ : P'.pairSupport₀₁ ⊆ P.pairSupport₀₁) (h₀₂ : P'.pairSupport₀₂ ⊆ P.pairSupport₀₂) (h₁₂ : P'.pairSupport₁₂ ⊆ P.pairSupport₁₂) (Q : Subpolyad3 P') : (inclusion h₀₁ h₀₂ h₁₂ Q).pair₁₂ = Q.pair₁₂

A subpolyad and its inclusion select the same pairs on roles one and two.

@[simp]

theorem TauCeti.Subpolyad3.support_inclusion {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {κ' : Type u_3} {S' : PairSkeleton3 κ' V} {P' : Polyad3 S'} (h₀₁ : P'.pairSupport₀₁ ⊆ P.pairSupport₀₁) (h₀₂ : P'.pairSupport₀₂ ⊆ P.pairSupport₀₂) (h₁₂ : P'.pairSupport₁₂ ⊆ P.pairSupport₁₂) (Q : Subpolyad3 P') : (inclusion h₀₁ h₀₂ h₁₂ Q).support = Q.support

Including a subpolyad does not change its support.

noncomputable def TauCeti.Subpolyad3.restrict {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {κ' : Type u_3} {S' : PairSkeleton3 κ' V} {P' : Polyad3 S'} (Q : Subpolyad3 P') (P : Polyad3 S) : Subpolyad3 P

The restriction of a subpolyad of P' to a polyad P, possibly over another skeleton: each selected pair graph is intersected with the corresponding pair graph of P. Its support consists of the triples supported by both the subpolyad and P.

@[simp]

theorem TauCeti.Subpolyad3.restrict_pair₀₁ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {κ' : Type u_3} {S' : PairSkeleton3 κ' V} {P' : Polyad3 S'} (Q : Subpolyad3 P') (P : Polyad3 S) : (Q.restrict P).pair₀₁ = Q.pair₀₁ ∩ P.pairSupport₀₁

The restriction keeps the selected zero-one pairs lying in the pair graph of P.

@[simp]

theorem TauCeti.Subpolyad3.restrict_pair₀₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {κ' : Type u_3} {S' : PairSkeleton3 κ' V} {P' : Polyad3 S'} (Q : Subpolyad3 P') (P : Polyad3 S) : (Q.restrict P).pair₀₂ = Q.pair₀₂ ∩ P.pairSupport₀₂

The restriction keeps the selected zero-two pairs lying in the pair graph of P.

@[simp]

theorem TauCeti.Subpolyad3.restrict_pair₁₂ {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {κ' : Type u_3} {S' : PairSkeleton3 κ' V} {P' : Polyad3 S'} (Q : Subpolyad3 P') (P : Polyad3 S) : (Q.restrict P).pair₁₂ = Q.pair₁₂ ∩ P.pairSupport₁₂

The restriction keeps the selected one-two pairs lying in the pair graph of P.

@[simp]

theorem TauCeti.Subpolyad3.support_restrict {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {κ' : Type u_3} {S' : PairSkeleton3 κ' V} {P' : Polyad3 S'} (Q : Subpolyad3 P') (P : Polyad3 S) : (Q.restrict P).support = Q.support ∩ P.support

The support of a restriction is the part of the original support lying in P.

noncomputable def TauCeti.Subpolyad3.unionSupport {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} [Fintype ι] (Q : ι → Subpolyad3 P) : Finset { x : Fin 3 → V // Function.Injective x }

The union of the supports of a finite family of subpolyads of P.

theorem TauCeti.Subpolyad3.unionSupport_def {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} [Fintype ι] (Q : ι → Subpolyad3 P) : unionSupport Q = Finset.univ.biUnion fun (i : ι) => (Q i).support

The union support is the finite union of the members' supports.

@[simp]

theorem TauCeti.Subpolyad3.mem_unionSupport {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} [Fintype ι] {Q : ι → Subpolyad3 P} {x : { x : Fin 3 → V // Function.Injective x }} : x ∈ unionSupport Q ↔ ∃ (i : ι), x ∈ (Q i).support

A triple lies in the union support when it lies in the support of some member.

theorem TauCeti.Subpolyad3.support_subset_unionSupport {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} [Fintype ι] (Q : ι → Subpolyad3 P) (i : ι) : (Q i).support ⊆ unionSupport Q

Each member's support lies in the union support.

theorem TauCeti.Subpolyad3.unionSupport_subset {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} [Fintype ι] (Q : ι → Subpolyad3 P) : unionSupport Q ⊆ P.support

The union support lies in the support of the parent polyad.

@[simp]

theorem TauCeti.Subpolyad3.unionSupport_of_isEmpty {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} [Fintype ι] [IsEmpty ι] (Q : ι → Subpolyad3 P) : unionSupport Q = ∅

The empty family has empty union support.

@[simp]

theorem TauCeti.Subpolyad3.unionSupport_unique {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} [Fintype ι] [Unique ι] (Q : ι → Subpolyad3 P) : unionSupport Q = (Q default).support

A family with a single member has that member's support as union support.

theorem TauCeti.Subpolyad3.exists_unionSupport_eq_of_card_le {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} [Fintype ι] {r : ℕ} (Q : ι → Subpolyad3 P) (hr : Fintype.card ι ≤ r) : ∃ (Q' : Fin r → Subpolyad3 P), unionSupport Q' = unionSupport Q

A family of at most r subpolyads has the same union support as a family indexed by Fin r, padded by the restriction to empty vertex sets.

@[simp]

theorem TauCeti.Subpolyad3.unionSupport_inclusion {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {P : Polyad3 S} {ι : Type u_3} [Fintype ι] {κ' : Type u_4} {S' : PairSkeleton3 κ' V} {P' : Polyad3 S'} (h₀₁ : P'.pairSupport₀₁ ⊆ P.pairSupport₀₁) (h₀₂ : P'.pairSupport₀₂ ⊆ P.pairSupport₀₂) (h₁₂ : P'.pairSupport₁₂ ⊆ P.pairSupport₁₂) (Q : ι → Subpolyad3 P') : (unionSupport fun (i : ι) => inclusion h₀₁ h₀₂ h₁₂ (Q i)) = unionSupport Q

Including every member of a family of subpolyads does not change its union support.

@[simp]

theorem TauCeti.Subpolyad3.unionSupport_restrict {κ : Type u_1} {V : Type u_2} [Fintype V] [DecidableEq V] {S : PairSkeleton3 κ V} {ι : Type u_3} [Fintype ι] {κ' : Type u_4} {S' : PairSkeleton3 κ' V} {P' : Polyad3 S'} (Q : ι → Subpolyad3 P') (P : Polyad3 S) : (unionSupport fun (i : ι) => (Q i).restrict P) = unionSupport Q ∩ P.support

Restricting every member of a family to P restricts its union support to P.