Built with
doc-gen4 , running Lean4.
Bubbles (
) indicate interactive fragments: hover for details, tap to reveal contents.
Use
Ctrl+↑ Ctrl+↓ to navigate,
Ctrl+🖱️ to focus.
On Mac, use
Cmd instead of
Ctrl .
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro, Oliver Nash
! This file was ported from Lean 3 source module data.finset.prod
! leanprover-community/mathlib commit 9003f28797c0664a49e4179487267c494477d853
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Finset.Card
/-!
# Finsets in product types
This file defines finset constructions on the product type `α × β`. Beware not to confuse with the
`Finset.prod` operation which computes the multiplicative product.
## Main declarations
* `Finset.product`: Turns `s : Finset α`, `t : Finset β` into their product in `Finset (α × β)`.
* `Finset.diag`: For `s : Finset α`, `s.diag` is the `Finset (α × α)` of pairs `(a, a)` with
`a ∈ s`.
* `Finset.offDiag`: For `s : Finset α`, `s.offDiag` is the `Finset (α × α)` of pairs `(a, b)` with
`a, b ∈ s` and `a ≠ b`.
-/
open Multiset
variable { α β γ : Type _ : Type (?u.67086+1)}
namespace Finset
/-! ### prod -/
section Prod
variable { s s' : Finset α } { t t' : Finset β } { a : α } { b : β }
/-- `product s t` is the set of pairs `(a, b)` such that `a ∈ s` and `b ∈ t`. -/
protected def product ( s : Finset α ) ( t : Finset β ) : Finset ( α × β ) :=
⟨ _ , s . nodup . product t . nodup ⟩
#align finset.product Finset.product
instance instSProd : SProd ( Finset α ) ( Finset β ) ( Finset ( α × β )) where
sprod := Finset.product
@[ simp ]
theorem product_val : ( s ×ˢ t ). 1 = s . 1 ×ˢ t . 1 :=
rfl : ∀ {α : Sort ?u.455} {a : α }, a = a
#align finset.product_val Finset.product_val
@[ simp ]
theorem mem_product { p : α × β } : p ∈ s ×ˢ t ↔ p . 1 : {α : Type ?u.569} → {β : Type ?u.568} → α × β α ∈ s ∧ p . 2 : {α : Type ?u.588} → {β : Type ?u.587} → α × β β ∈ t :=
Multiset.mem_product
#align finset.mem_product Finset.mem_product
theorem mk_mem_product : a ∈ s b ∈ t (a , b ) ∈ s ×ˢ t mk_mem_product ( ha : a ∈ s ) ( hb : b ∈ t ) : ( a , b ) ∈ s ×ˢ t :=
mem_product . 2 : ∀ {a b : Prop }, (a ↔ b b → a ⟨ ha , hb ⟩
#align finset.mk_mem_product Finset.mk_mem_product : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α t : Finset β a : α } {b : β }, a ∈ s b ∈ t (a , b ) ∈ s ×ˢ t
@[ simp , norm_cast ]
theorem coe_product ( s : Finset α ) ( t : Finset β ) :
(↑( s ×ˢ t ) : Set ( α × β )) = ( s : Set α ) ×ˢ t :=
Set.ext : ∀ {α : Type ?u.1392} {a b : Set α (∀ (x : α ), x ∈ a ↔ x ∈ b ) → a = b fun _ => Finset.mem_product
#align finset.coe_product Finset.coe_product
theorem subset_product_image_fst [ DecidableEq : Sort ?u.1602 → Sort (max1?u.1602) α ] : ( s ×ˢ t ). image Prod.fst : {α : Type ?u.1721} → {β : Type ?u.1720} → α × β α ⊆ s := fun i => by
simp ( config := { contextual := true }) [ mem_image ]
#align finset.subset_product_image_fst Finset.subset_product_image_fst
theorem subset_product_image_snd [ DecidableEq : Sort ?u.6752 → Sort (max1?u.6752) β ] : ( s ×ˢ t ). image Prod.snd : {α : Type ?u.6871} → {β : Type ?u.6870} → α × β β ⊆ t := fun i => by
simp ( config := { contextual := true }) [ mem_image ]
#align finset.subset_product_image_snd Finset.subset_product_image_snd
theorem product_image_fst [ DecidableEq : Sort ?u.11271 → Sort (max1?u.11271) α ] ( ht : t . Nonempty ) : ( s ×ˢ t ). image Prod.fst : {α : Type ?u.11332} → {β : Type ?u.11331} → α × β α = s := by
ext i
simp [ mem_image , ht . bex ]
#align finset.product_image_fst Finset.product_image_fst
theorem product_image_snd [ DecidableEq : Sort ?u.13955 → Sort (max1?u.13955) β ] ( ht : s . Nonempty ) : ( s ×ˢ t ). image Prod.snd : {α : Type ?u.14016} → {β : Type ?u.14015} → α × β β = t := by
ext i
simp [ mem_image , ht . bex ]
#align finset.product_image_snd Finset.product_image_snd
theorem subset_product [ DecidableEq : Sort ?u.16402 → Sort (max1?u.16402) α ] [ DecidableEq : Sort ?u.16411 → Sort (max1?u.16411) β ] { s : Finset ( α × β )} :
s ⊆ s . image Prod.fst : {α : Type ?u.16452} → {β : Type ?u.16451} → α × β α ×ˢ s . image Prod.snd : {α : Type ?u.16519} → {β : Type ?u.16518} → α × β β := fun _ hp =>
mem_product . 2 : ∀ {a b : Prop }, (a ↔ b b → a ⟨ mem_image_of_mem _ hp , mem_image_of_mem _ hp ⟩
#align finset.subset_product Finset.subset_product
theorem product_subset_product ( hs : s ⊆ s' ) ( ht : t ⊆ t' ) : s ×ˢ t ⊆ s' ×ˢ t' := fun ⟨_, _⟩ h =>
mem_product . 2 : ∀ {a b : Prop }, (a ↔ b b → a ⟨ hs ( mem_product . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ). 1 : ∀ {a b : Prop }, a ∧ b a , ht ( mem_product . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ). 2 : ∀ {a b : Prop }, a ∧ b b ⟩
#align finset.product_subset_product Finset.product_subset_product : ∀ {α : Type u_1} {β : Type u_2} {s s' : Finset α t t' : Finset β s ⊆ s' t ⊆ t' s ×ˢ t ⊆ s' ×ˢ t'
theorem product_subset_product_left ( hs : s ⊆ s' ) : s ×ˢ t ⊆ s' ×ˢ t :=
product_subset_product : ∀ {α : Type ?u.17463} {β : Type ?u.17464} {s s' : Finset α t t' : Finset β s ⊆ s' t ⊆ t' s ×ˢ t ⊆ s' ×ˢ t' hs ( Subset.refl : ∀ {α : Type ?u.17491} (s : Finset α s ⊆ s _ )
#align finset.product_subset_product_left Finset.product_subset_product_left
theorem product_subset_product_right : t ⊆ t' s ×ˢ t ⊆ s ×ˢ t' product_subset_product_right ( ht : t ⊆ t' ) : s ×ˢ t ⊆ s ×ˢ t' :=
product_subset_product : ∀ {α : Type ?u.17635} {β : Type ?u.17636} {s s' : Finset α t t' : Finset β s ⊆ s' t ⊆ t' s ×ˢ t ⊆ s' ×ˢ t' ( Subset.refl : ∀ {α : Type ?u.17663} (s : Finset α s ⊆ s _ ) ht
#align finset.product_subset_product_right Finset.product_subset_product_right
theorem map_swap_product ( s : Finset α ) ( t : Finset β ) :
( t ×ˢ s ). map ⟨ Prod.swap : {α : Type ?u.17762} → {β : Type ?u.17761} → α × β β × α , Prod.swap_injective ⟩ = s ×ˢ t :=
coe_injective <| by
push_cast
exact Set.image_swap_prod : ∀ {α : Type ?u.18194} {β : Type ?u.18195} (s : Set α t : Set β Prod.swap '' s ×ˢ t = t ×ˢ s _ _
#align finset.map_swap_product Finset.map_swap_product
@[ simp ]
theorem image_swap_product [ DecidableEq : Sort ?u.18253 → Sort (max1?u.18253) ( α × β )] ( s : Finset α ) ( t : Finset β ) :
( t ×ˢ s ). image Prod.swap : {α : Type ?u.18316} → {β : Type ?u.18315} → α × β β × α = s ×ˢ t :=
coe_injective <| by
push_cast
exact Set.image_swap_prod : ∀ {α : Type ?u.18757} {β : Type ?u.18758} (s : Set α t : Set β Prod.swap '' s ×ˢ t = t ×ˢ s _ _
#align finset.image_swap_product Finset.image_swap_product
theorem product_eq_biUnion [ DecidableEq : Sort ?u.18861 → Sort (max1?u.18861) ( α × β )] ( s : Finset α ) ( t : Finset β ) :
s ×ˢ t = s . biUnion fun a => t . image fun b => ( a , b ) :=
ext : ∀ {α : Type ?u.19081} {s₁ s₂ : Finset α (∀ (a : α ), a ∈ s₁ ↔ a ∈ s₂ ) → s₁ = s₂ fun ⟨ x , y ⟩ => by
simp only [ mem_product , mem_biUnion , mem_image , exists_prop : ∀ {b a : Prop }, (∃ _h , b ) ↔ a ∧ b , Prod.mk.inj_iff : ∀ {α : Type ?u.19351} {β : Type ?u.19352} {a₁ a₂ : α } {b₁ b₂ : β }, (a₁ , b₁ ) = (a₂ , b₂ ) ↔ a₁ = a₂ ∧ b₁ = b₂ , and_left_comm : ∀ {a b c : Prop }, a ∧ b ∧ c ↔ b ∧ a ∧ c ,
exists_and_left : ∀ {α : Sort ?u.19401} {p : α → Prop b : Prop }, (∃ x , b ∧ p x ) ↔ b ∧ ∃ x , p x , exists_eq_right : ∀ {α : Sort ?u.19419} {p : α → Prop a' : α }, (∃ a , p a ∧ a = a' ) ↔ p a' , exists_eq_left : ∀ {α : Sort ?u.19437} {p : α → Prop a' : α }, (∃ a , a = a' ∧ p a ) ↔ p a' ]
#align finset.product_eq_bUnion Finset.product_eq_biUnion
theorem product_eq_biUnion_right [ DecidableEq : Sort ?u.20077 → Sort (max1?u.20077) ( α × β )] ( s : Finset α ) ( t : Finset β ) :
s ×ˢ t = t . biUnion fun b => s . image fun a => ( a , b ) :=
ext : ∀ {α : Type ?u.20297} {s₁ s₂ : Finset α (∀ (a : α ), a ∈ s₁ ↔ a ∈ s₂ ) → s₁ = s₂ fun ⟨ x , y ⟩ => by
simp only [ mem_product , mem_biUnion , mem_image , exists_prop : ∀ {b a : Prop }, (∃ _h , b ) ↔ a ∧ b , Prod.mk.inj_iff : ∀ {α : Type ?u.20553} {β : Type ?u.20554} {a₁ a₂ : α } {b₁ b₂ : β }, (a₁ , b₁ ) = (a₂ , b₂ ) ↔ a₁ = a₂ ∧ b₁ = b₂ , and_left_comm : ∀ {a b c : Prop }, a ∧ b ∧ c ↔ b ∧ a ∧ c ,
exists_and_left : ∀ {α : Sort ?u.20597} {p : α → Prop b : Prop }, (∃ x , b ∧ p x ) ↔ b ∧ ∃ x , p x , exists_eq_right : ∀ {α : Sort ?u.20613} {p : α → Prop a' : α }, (∃ a , p a ∧ a = a' ) ↔ p a' , exists_eq_left : ∀ {α : Sort ?u.20626} {p : α → Prop a' : α }, (∃ a , a = a' ∧ p a ) ↔ p a' ]
#align finset.product_eq_bUnion_right Finset.product_eq_biUnion_right
/-- See also `Finset.sup_product_left`. -/
@[ simp ]
theorem product_biUnion [ DecidableEq : Sort ?u.21232 → Sort (max1?u.21232) γ ] ( s : Finset α ) ( t : Finset β ) ( f : α × β → Finset γ ) :
( s ×ˢ t ). biUnion f = s . biUnion fun a => t . biUnion fun b => f ( a , b ) := by
classical simp_rw [ product_eq_biUnion , biUnion_biUnion , image_biUnion ]
#align finset.product_bUnion Finset.product_biUnion
@[ simp ]
theorem card_product ( s : Finset α ) ( t : Finset β ) : card ( s ×ˢ t ) = card s * card t :=
Multiset.card_product : ∀ {α : Type ?u.23070} {β : Type ?u.23071} (s : Multiset α t : Multiset β ↑Multiset.card (s ×ˢ t = ↑Multiset.card s * ↑Multiset.card t _ _
#align finset.card_product Finset.card_product
theorem filter_product ( p : α → Prop ) ( q : β → Prop ) [ DecidablePred : {α : Sort ?u.23189} → (α → Prop Sort (max1?u.23189) p ] [ DecidablePred : {α : Sort ?u.23199} → (α → Prop Sort (max1?u.23199) q ] :
(( s ×ˢ t ). filter fun x : α × β => p x . 1 : {α : Type ?u.23254} → {β : Type ?u.23253} → α × β α ∧ q x . 2 : {α : Type ?u.23260} → {β : Type ?u.23259} → α × β β ) = s . filter p ×ˢ t . filter q := by
ext ⟨ a , b ⟩
simp [ mem_filter , mem_product , decide_eq_true_eq , and_comm : ∀ {a b : Prop }, a ∧ b ↔ b ∧ a , and_left_comm : ∀ {a b c : Prop }, a ∧ b ∧ c ↔ b ∧ a ∧ c , and_assoc : ∀ {a b c : Prop }, (a ∧ b ∧ c ↔ a ∧ b ∧ c ]
#align finset.filter_product Finset.filter_product
theorem filter_product_left ( p : α → Prop ) [ DecidablePred : {α : Sort ?u.28929} → (α → Prop Sort (max1?u.28929) p ] :
(( s ×ˢ t ). filter fun x : α × β => p x . 1 : {α : Type ?u.28984} → {β : Type ?u.28983} → α × β α ) = s . filter p ×ˢ t := by
simpa using filter_product p fun _ => true
#align finset.filter_product_left Finset.filter_product_left
theorem filter_product_right ( q : β → Prop ) [ DecidablePred : {α : Sort ?u.45801} → (α → Prop Sort (max1?u.45801) q ] :
(( s ×ˢ t ). filter fun x : α × β => q x . 2 : {α : Type ?u.45856} → {β : Type ?u.45855} → α × β β ) = s ×ˢ t . filter q := by
simpa using filter_product ( fun _ : α => true ) q
#align finset.filter_product_right Finset.filter_product_right
theorem filter_product_card ( s : Finset α ) ( t : Finset β ) ( p : α → Prop ) ( q : β → Prop )
[ DecidablePred : {α : Sort ?u.63155} → (α → Prop Sort (max1?u.63155) p ] [ DecidablePred : {α : Sort ?u.63165} → (α → Prop Sort (max1?u.63165) q ] :
(( s ×ˢ t ). filter fun x : α × β => ( p x . 1 : {α : Type ?u.63221} → {β : Type ?u.63220} → α × β α ) = ( q x . 2 : {α : Type ?u.63227} → {β : Type ?u.63226} → α × β β )). card =
( s . filter p ). card * ( t . filter q ). card +
( s . filter (¬ p ·)). card * ( t . filter (¬ q ·)). card := by
classical
rw [ ← card_product , ← card_product , ← filter_product , ← filter_product , ← card_union_eq ]
· apply congr_arg : ∀ {α : Sort ?u.64516} {β : Sort ?u.64515} {a₁ a₂ : α } (f : α → β a₁ = a₂ f a₁ = f a₂
ext ⟨ a , b ⟩
simp only [ filter_union_right , mem_filter , mem_product ]
constructor h.a.mk.mp (a ∈ s ∧ b ∈ t ∧ p a = q b → (a ∈ s ∧ b ∈ t ∧ (p a ∧ q b ∨ ¬ p a ∧ ¬ q b h.a.mk.mpr (a ∈ s ∧ b ∈ t ∧ (p a ∧ q b ∨ ¬ p a ∧ ¬ q b → (a ∈ s ∧ b ∈ t ∧ p a = q b <;> h.a.mk.mp (a ∈ s ∧ b ∈ t ∧ p a = q b → (a ∈ s ∧ b ∈ t ∧ (p a ∧ q b ∨ ¬ p a ∧ ¬ q b h.a.mk.mpr (a ∈ s ∧ b ∈ t ∧ (p a ∧ q b ∨ ¬ p a ∧ ¬ q b → (a ∈ s ∧ b ∈ t ∧ p a = q b intro h <;> h.a.mk.mp h.a.mk.mpr (a ∈ s ∧ b ∈ t ∧ p a = q b use h . 1 : ∀ {a b : Prop }, a ∧ b a
. simp only [ h . 2 : ∀ {a b : Prop }, a ∧ b b , Function.comp_apply : ∀ {β : Sort ?u.65473} {δ : Sort ?u.65474} {α : Sort ?u.65475} {f : β → δ g : α → β x : α }, (f ∘ g ) x = f (g x , Decidable.em , and_self : ∀ (p : Prop ), (p ∧ p = p ]
. revert h h.a.mk.mpr (a ∈ s ∧ b ∈ t ∧ (p a ∧ q b ∨ ¬ p a ∧ ¬ q b → p a = q b
simp only [ Function.comp_apply : ∀ {β : Sort ?u.65554} {δ : Sort ?u.65555} {α : Sort ?u.65556} {f : β → δ g : α → β x : α }, (f ∘ g ) x = f (g x , and_imp : ∀ {a b c : Prop }, a ∧ b c ↔ a → b → c ] h.a.mk.mpr a ∈ s b ∈ t p a ∧ q b ∨ ¬ p a ∧ ¬ q b p a = q b
rintro _ _ (_|_) : p a ∧ q b ∨ ¬ p a ∧ ¬ q b _ _|_ : p a ∧ q b ∨ ¬ p a ∧ ¬ q b _ (_|_) : p a ∧ q b ∨ ¬ p a ∧ ¬ q b h.a.mk.mpr.inl h.a.mk.mpr.inr h.a.mk.mpr a ∈ s b ∈ t p a ∧ q b ∨ ¬ p a ∧ ¬ q b p a = q b <;> h.a.mk.mpr.inl h.a.mk.mpr.inr h.a.mk.mpr a ∈ s b ∈ t p a ∧ q b ∨ ¬ p a ∧ ¬ q b p a = q b simp [*]
· apply Finset.disjoint_filter_filter'
exact ( disjoint_compl_right . inf_left _ ). inf_right _
#align finset.filter_product_card Finset.filter_product_card
theorem empty_product ( t : Finset β ) : ( ∅ : Finset α ) ×ˢ t = ∅ :=
rfl : ∀ {α : Sort ?u.66781} {a : α }, a = a
#align finset.empty_product Finset.empty_product
theorem product_empty ( s : Finset α ) : s ×ˢ ( ∅ : Finset β ) = ∅ :=
eq_empty_of_forall_not_mem : ∀ {α : Type ?u.67017} {s : Finset α (∀ (x : α ), ¬ x ∈ s ) → s = ∅ fun _ h => not_mem_empty : ∀ {α : Type ?u.67030} (a : α ), ¬ a ∈ ∅ _ ( Finset.mem_product . 1 : ∀ {a b : Prop }, (a ↔ b a → b h ). 2 : ∀ {a b : Prop }, a ∧ b b
#align finset.product_empty Finset.product_empty
theorem Nonempty.product ( hs : s . Nonempty ) ( ht : t . Nonempty ) : ( s ×ˢ t ). Nonempty :=
let ⟨ x , hx ⟩ := hs
let ⟨ y , hy ⟩ := ht
⟨( x , y ), mem_product . 2 : ∀ {a b : Prop }, (a ↔ b b → a ⟨ hx , hy ⟩⟩
#align finset.nonempty.product Finset.Nonempty.product
theorem Nonempty.fst ( h : ( s ×ˢ t ). Nonempty ) : s . Nonempty :=
let ⟨ xy , hxy ⟩ := h
⟨ xy . 1 : {α : Type ?u.67542} → {β : Type ?u.67541} → α × β α , ( mem_product . 1 : ∀ {a b : Prop }, (a ↔ b a → b hxy ). 1 : ∀ {a b : Prop }, a ∧ b a ⟩
#align finset.nonempty.fst Finset.Nonempty.fst
theorem Nonempty.snd ( h : ( s ×ˢ t ). Nonempty ) : t . Nonempty :=
let ⟨ xy , hxy ⟩ := h
⟨ xy . 2 : {α : Type ?u.67782} → {β : Type ?u.67781} → α × β β , ( mem_product . 1 : ∀ {a b : Prop }, (a ↔ b a → b hxy ). 2 : ∀ {a b : Prop }, a ∧ b b ⟩
#align finset.nonempty.snd Finset.Nonempty.snd
@[ simp ]
theorem nonempty_product : ( s ×ˢ t ). Nonempty ↔ s . Nonempty ∧ t . Nonempty :=
⟨ fun h => ⟨ h . fst , h . snd ⟩, fun h => h . 1 : ∀ {a b : Prop }, a ∧ b a . product h . 2 : ∀ {a b : Prop }, a ∧ b b ⟩
#align finset.nonempty_product Finset.nonempty_product
@[ simp ]
theorem product_eq_empty { s : Finset α } { t : Finset β } : s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅ := by
rw [ ← not_nonempty_iff_eq_empty , nonempty_product , not_and_or , not_nonempty_iff_eq_empty ,
not_nonempty_iff_eq_empty ]
#align finset.product_eq_empty Finset.product_eq_empty
@[ simp ]
theorem singleton_product { a : α } :
({ a } : Finset α ) ×ˢ t = t . map ⟨ Prod.mk : {α : Type ?u.68631} → {β : Type ?u.68630} → α → β → α × β a , Prod.mk.inj_left _ ⟩ := by
ext ⟨ x , y ⟩
simp [ and_left_comm : ∀ {a b c : Prop }, a ∧ b ∧ c ↔ b ∧ a ∧ c , eq_comm : ∀ {α : Sort ?u.68731} {a b : α }, a = b ↔ b = a ]
#align finset.singleton_product Finset.singleton_product
@[ simp ]
theorem product_singleton { b : β } : s ×ˢ { b } = s . map ⟨ fun i => ( i , b ), Prod.mk.inj_right _ ⟩ := by
ext ⟨ x , y ⟩
simp [ and_left_comm : ∀ {a b c : Prop }, a ∧ b ∧ c ↔ b ∧ a ∧ c , eq_comm : ∀ {α : Sort ?u.70458} {a b : α }, a = b ↔ b = a ]
#align finset.product_singleton Finset.product_singleton
theorem singleton_product_singleton : ∀ {a : α } {b : β }, {a } ×ˢ {b } = {(a , b ) } singleton_product_singleton { a : α } { b : β } :
({ a } ×ˢ { b } : Finset _ ) = {( a , b )} := by
simp only [ product_singleton , Function.Embedding.coeFn_mk : ∀ {α : Sort ?u.72051} {β : Sort ?u.72052} (f : α → β i : Function.Injective f ↑{ toFun := f , inj' := i } = f , map_singleton : ∀ {α : Type ?u.72079} {β : Type ?u.72080} (f : α ↪ β a : α ), map f {a } = {↑f a } ]
#align finset.singleton_product_singleton Finset.singleton_product_singleton : ∀ {α : Type u_1} {β : Type u_2} {a : α } {b : β }, {a } ×ˢ {b } = {(a , b ) }
@[ simp ]
theorem union_product [ DecidableEq : Sort ?u.72412 → Sort (max1?u.72412) α ] [ DecidableEq : Sort ?u.72421 → Sort (max1?u.72421) β ] : ( s ∪ s' ) ×ˢ t = s ×ˢ t ∪ s' ×ˢ t := by
ext ⟨ x , y ⟩
simp only [ or_and_right : ∀ {a b c : Prop }, (a ∨ b ∧ c ↔ a ∧ c ∨ b ∧ c ,