Supporting results for pointwise provable equality.

class PointwiseComposition.Adjoin (β : outParam (Type u_1)) (α : Type u_2) : Type (max u_1 u_2)

Data and laws for Adjoin in Adjoin.

• adjoin : β → α → α

  The adjoin construction in adjoin.

@[instance_reducible]

instance PointwiseComposition.instAdjoinSet (α : Type u_1) : Adjoin α (Set α)

Equations

• PointwiseComposition.instAdjoinSet α = { adjoin := insert }

@[instance_reducible]

instance PointwiseComposition.instAdjoinList (α : Type u_1) : Adjoin α (List α)

Equations

• PointwiseComposition.instAdjoinList α = { adjoin := List.cons }

@[instance_reducible]

instance PointwiseComposition.instAdjoinMultiset (α : Type u_1) : Adjoin α (Multiset α)

Equations

• PointwiseComposition.instAdjoinMultiset α = { adjoin := Multiset.cons }

@[instance_reducible]

instance PointwiseComposition.instAdjoinFinsetOfDecidableEq (α : Type u_1) [DecidableEq α] : Adjoin α (Finset α)

Equations

• PointwiseComposition.instAdjoinFinsetOfDecidableEq α = { adjoin := insert }

class PointwiseComposition.AdjunctiveSet (β : outParam (Type u_1)) (α : Type u_2) extends Membership β α, HasSubset α, EmptyCollection α, PointwiseComposition.Adjoin β α : Type (max u_1 u_2)

Data and laws for Adjunctive Set in AdjunctiveSet.

• mem : α → β → Prop
• Subset : α → α → Prop
• emptyCollection : α
• adjoin : β → α → α
• subset_iff {a b : α} : a ⊆ b ↔ ∀ x ∈ a, x ∈ b
• not_mem_empty (x : β) : x ∉ ∅
• mem_cons_iff {x z : β} {a : α} : x ∈ adjoin z a ↔ x = z ∨ x ∈ a

@[instance_reducible]

instance PointwiseComposition.Set.adjunctiveSet {α : Type u_1} : AdjunctiveSet α (Set α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance PointwiseComposition.List.adjunctiveSet {α : Type u_1} : AdjunctiveSet α (List α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance PointwiseComposition.Multiset.adjunctiveSet {α : Type u_1} : AdjunctiveSet α (Multiset α)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance PointwiseComposition.Finset.adjunctiveSet {α : Type u_1} [DecidableEq α] : AdjunctiveSet α (Finset α)

Equations

• One or more equations did not get rendered due to their size.

def PointwiseComposition.AdjunctiveSet.set {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] : α → Set β

The set construction in AdjunctiveSet.

Equations

• PointwiseComposition.AdjunctiveSet.set a = {x : β | x ∈ a}

@[simp]

theorem PointwiseComposition.AdjunctiveSet.mem_set_iff {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {x : β} {a : α} : x ∈ set a ↔ x ∈ a

theorem PointwiseComposition.AdjunctiveSet.subset_iff_set_subset_set {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {a b : α} : a ⊆ b ↔ set a ⊆ set b

@[simp]

theorem PointwiseComposition.AdjunctiveSet.subset_refl {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (a : α) : a ⊆ a

theorem PointwiseComposition.AdjunctiveSet.subset_trans {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {a b c : α} (ha : a ⊆ b) (hb : b ⊆ c) : a ⊆ c

theorem PointwiseComposition.AdjunctiveSet.subset_antisymm {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {a b : α} (ha : a ⊆ b) (hb : b ⊆ a) : set a = set b

@[simp]

theorem PointwiseComposition.AdjunctiveSet.empty_subset {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (a : α) : ∅ ⊆ a

theorem PointwiseComposition.AdjunctiveSet.mem_cons {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (a : α) (x : β) : x ∈ adjoin x a

@[simp]

theorem PointwiseComposition.AdjunctiveSet.subset_cons {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (a : α) (x : β) : a ⊆ adjoin x a

@[simp]

theorem PointwiseComposition.AdjunctiveSet.set_empty {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] : set ∅ = ∅

@[simp]

theorem PointwiseComposition.AdjunctiveSet.set_cons {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (z : β) (a : α) : set (adjoin z a) = insert z (set a)

def PointwiseComposition.AdjunctiveSet.Finite {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (a : α) : Prop

The Finite construction in AdjunctiveSet.

Equations

• PointwiseComposition.AdjunctiveSet.Finite a = (PointwiseComposition.AdjunctiveSet.set a).Finite

@[simp]

theorem PointwiseComposition.AdjunctiveSet.empty_finite {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] : Finite ∅

theorem PointwiseComposition.AdjunctiveSet.Finite.of_subset {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {a b : α} (ha : Finite a) (h : b ⊆ a) : Finite b

@[simp]

theorem PointwiseComposition.AdjunctiveSet.cons_finite_iff {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {z : β} {a : α} : Finite (adjoin z a) ↔ Finite a

def PointwiseComposition.AdjunctiveSet.addList {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (a : α) : List β → α

The add List construction in AdjunctiveSet.

Equations

• PointwiseComposition.AdjunctiveSet.addList a [] = a
• PointwiseComposition.AdjunctiveSet.addList a (x_1 :: xs) = PointwiseComposition.adjoin x_1 (PointwiseComposition.AdjunctiveSet.addList a xs)

def PointwiseComposition.List.toAdjunctiveSet {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] : List β → α

The to Adjunctive Set construction in List.

Equations

• PointwiseComposition.List.toAdjunctiveSet [] = ∅
• PointwiseComposition.List.toAdjunctiveSet (x_1 :: xs) = PointwiseComposition.adjoin x_1 (PointwiseComposition.List.toAdjunctiveSet xs)

noncomputable def PointwiseComposition.Finset.toAdjunctiveSet {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] : Finset β → α

The to Adjunctive Set construction in Finset.

Equations

• PointwiseComposition.Finset.toAdjunctiveSet s = PointwiseComposition.List.toAdjunctiveSet s.toList

@[simp]

theorem PointwiseComposition.AdjunctiveSet.mem_list_toAdjunctiveSet {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {x : β} {l : List β} : x ∈ List.toAdjunctiveSet l ↔ x ∈ l

@[simp]

theorem PointwiseComposition.AdjunctiveSet.mem_finset_toAdjunctiveSet {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] {x : β} {s : Finset β} : x ∈ Finset.toAdjunctiveSet s ↔ x ∈ s

@[simp]

theorem PointwiseComposition.AdjunctiveSet.list_toAdjunctiveSet_finite {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (l : List β) : Finite (List.toAdjunctiveSet l)

@[simp]

theorem PointwiseComposition.AdjunctiveSet.finset_toAdjunctiveSet_finite {β : Type u_1} {α : Type u_2} [AdjunctiveSet β α] (s : Finset β) : Finite (Finset.toAdjunctiveSet s)

theorem PointwiseComposition.Set.cons_eq {α : Type u_1} (a : α) (s : Set α) : adjoin a s = insert a s

@[simp]

theorem PointwiseComposition.Set.adjunctiveSet_set {α : Type u_1} (s : Set α) : AdjunctiveSet.set s = s

@[simp]

theorem PointwiseComposition.Set.adjunctiveSet_finite_iff {α : Type u_1} (s : Set α) : AdjunctiveSet.Finite s ↔ s.Finite