Supporting results for pointwise provable equality.

theorem PointwiseComposition.Finset.doubleton_subset {α : Type u_1} {a b : α} {s : Finset α} [DecidableEq α] : {a, b} ⊆ s ↔ a ∈ s ∧ b ∈ s

theorem PointwiseComposition.Finset.no_ssubset_descending_chain {α : Type u_1} {f : ℕ → Finset α} : ¬∀ (i : ℕ), ∃ j > i, f j ⊂ f i

noncomputable def PointwiseComposition.Finset.rangeOfFinite {α : Type u_1} {ι : Sort v} [Finite ι] (f : ι → α) : Finset α

The range Of Finite construction in Finset.

Equations

• PointwiseComposition.Finset.rangeOfFinite f = ⋯.toFinset

theorem PointwiseComposition.Finset.mem_rangeOfFinite_iff {α : Type u_1} {ι : Sort v} [Finite ι] {f : ι → α} {a : α} : a ∈ rangeOfFinite f ↔ ∃ (i : ι), f i = a

noncomputable def PointwiseComposition.Finset.imageOfFinset {α : Type u_1} {β : Type u_2} [DecidableEq β] (s : Finset α) (f : (a : α) → a ∈ s → β) : Finset β

The image Of Finset construction in Finset.

Equations

• PointwiseComposition.Finset.imageOfFinset s f = s.biUnion fun (x : α) => PointwiseComposition.Finset.rangeOfFinite (f x)

theorem PointwiseComposition.Finset.mem_imageOfFinset_iff {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {f : (a : α) → a ∈ s → β} {b : β} : b ∈ imageOfFinset s f ↔ ∃ (a : α) (ha : a ∈ s), f a ha = b

@[simp]

theorem PointwiseComposition.Finset.mem_imageOfFinset {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} (f : (a : α) → a ∈ s → β) (a : α) (ha : a ∈ s) : f a ha ∈ imageOfFinset s f

theorem PointwiseComposition.Finset.erase_union {α : Type u_1} [DecidableEq α] {a : α} {s t : Finset α} : (s ∪ t).erase a = s.erase a ∪ t.erase a

theorem PointwiseComposition.Finset.equiv_univ {α : Type u_2} {α' : Type u_3} [Fintype α] [Fintype α'] [DecidableEq α'] (e : α ≃ α') : Finset.image (⇑e) Finset.univ = Finset.univ

@[simp]

theorem PointwiseComposition.Finset.sup_univ_equiv {β : Type u_2} {α : Type u_3} {α' : Type u_4} [Fintype α] [Fintype α'] [SemilatticeSup β] [OrderBot β] (f : α → β) (e : α' ≃ α) : (Finset.univ.sup fun (i : α') => f (e i)) = Finset.univ.sup f

theorem PointwiseComposition.Finset.sup_univ_cast {α : Type u_2} [SemilatticeSup α] [OrderBot α] {n : ℕ} (f : Fin n → α) (n' : ℕ) {h : n' = n} : (Finset.univ.sup fun (i : Fin n') => f (Fin.cast h i)) = Finset.univ.sup f

theorem PointwiseComposition.Finset.biUnion_eq_empty {α : Type u_1} {β : Type u_2} [DecidableEq β] {s : Finset α} {f : α → Finset β} : s.biUnion f = ∅ ↔ ∀ i ∈ s, f i = ∅