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 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
! This file was ported from Lean 3 source module data.fintype.prod
! leanprover-community/mathlib commit 509de852e1de55e1efa8eacfa11df0823f26f226
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.Fintype.Card
import Mathlib.Data.Finset.Prod
/-!
# fintype instance for the product of two fintypes.
-/
open Function
open Nat
universe u v
variable { α β γ : Type _ }
open Finset Function
namespace Set
variable { s t : Set α }
theorem toFinset_prod ( s : Set α ) ( t : Set β ) [ Fintype s ] [ Fintype t ] [ Fintype ( s ×ˢ t )] :
( s ×ˢ t ). toFinset = s . toFinset ×ˢ t . toFinset := by
ext
simp
#align set.to_finset_prod Set.toFinset_prod
theorem toFinset_off_diag { s : Set α } [ DecidableEq : Sort ?u.1009 → Sort (max1?u.1009) α ] [ Fintype s ] [ Fintype s . offDiag ] :
s . offDiag . toFinset = s . toFinset . offDiag :=
Finset.ext : ∀ {α : Type ?u.1377} {s₁ s₂ : Finset α (∀ (a : α ), a ∈ s₁ ↔ a ∈ s₂ ) → s₁ = s₂ <| by simp
#align set.to_finset_off_diag Set.toFinset_off_diag
end Set
instance ( α β : Type _ ) [ Fintype α ] [ Fintype β ] : Fintype ( α × β ) :=
⟨ univ ×ˢ univ , fun ⟨ a , b ⟩ => by simp ⟩
@[ simp ]
theorem Finset.univ_product_univ { α β : Type _ } [ Fintype α ] [ Fintype β ] :
( univ : Finset α ) ×ˢ ( univ : Finset β ) = univ :=
rfl : ∀ {α : Sort ?u.4279} {a : α }, a = a
#align finset.univ_product_univ Finset.univ_product_univ
@[ simp ]
theorem Fintype.card_prod ( α β : Type _ ) [ Fintype α ] [ Fintype β ] :
Fintype.card ( α × β ) = Fintype.card α * Fintype.card β :=
card_product _ _
#align fintype.card_prod Fintype.card_prod
section
open Classical
@[ simp ]
theorem infinite_prod : Infinite ( α × β ) ↔ Infinite α ∧ Nonempty β ∨ Nonempty α ∧ Infinite β := by
refine'
⟨ fun H => _ , fun H =>
H . elim : ∀ {a b c : Prop }, a ∨ b (a → c (b → c c ( and_imp : ∀ {a b c : Prop }, a ∧ b c ↔ a → b → c . 2 : ∀ {a b : Prop }, (a ↔ b b → a <| @ Prod.infinite_of_left α β ) ( and_imp : ∀ {a b c : Prop }, a ∧ b c ↔ a → b → c . 2 : ∀ {a b : Prop }, (a ↔ b b → a <| @ Prod.infinite_of_right α β )⟩
rw [ and_comm : ∀ {a b : Prop }, a ∧ b ↔ b ∧ a ] ; contrapose! H ; intro H'
rcases Infinite.nonempty ( α × β ) with ⟨ a , b ⟩
haveI := fintypeOfNotInfinite ( H . 1 : ∀ {a b : Prop }, a ∧ b a ⟨ b ⟩) ; haveI := fintypeOfNotInfinite ( H . 2 : ∀ {a b : Prop }, a ∧ b b ⟨ a ⟩)
exact H' . false
#align infinite_prod infinite_prod
instance Pi.infinite_of_left { ι : Sort _ } { π : ι → Sort _ } [∀ i , Nontrivial <| π i ] [ Infinite ι ] :
Infinite (∀ i : ι , π i ) := by
choose m n hm using fun i => exists_pair_ne ( π i )
refine' Infinite.of_injective ( fun i => update : {α : Sort ?u.4917} → {β : α → Sort ?u.4916[inst : DecidableEq α ((a : α ) → β a ) → (a' : α ) → β a' (a : α ) → β a m i ( n i )) fun x y h => of_not_not : ∀ {a : Prop }, ¬ ¬ a a fun hne => _
simp_rw [ update_eq_iff : ∀ {α : Sort ?u.5470} {β : α → Sort ?u.5469inst : DecidableEq α a : α } {b : β a f g : (a : α ) → β a },
update f a b = g ↔ b = g a ∧ ∀ (x : α ), x ≠ a f x = g x , update_noteq : ∀ {α : Sort ?u.6009} {β : α → Sort ?u.6008inst : DecidableEq α a a' : α },
a ≠ a' ∀ (v : β a' f : (a : α ) → β a ), update f a' v a = f a hne α : Type ?u.4802β : Type ?u.4805γ : Type ?u.4808ι : Sort ?u.4811π : ι → Type ?u.4823inst✝¹ : ∀ (i : ι ), Nontrivial (π i inst✝ : Infinite ι m, n : (i : ι ) → π i hm : ∀ (i : ι ), m i ≠ n i x, y : ι hne : ¬ x = y h : n x = m x ∧ ∀ (x_1 : ι ), x_1 ≠ x m x_1 = update m y (n y x_1 ] at h α : Type ?u.4802β : Type ?u.4805γ : Type ?u.4808ι : Sort ?u.4811π : ι → Type ?u.4823inst✝¹ : ∀ (i : ι ), Nontrivial (π i inst✝ : Infinite ι m, n : (i : ι ) → π i hm : ∀ (i : ι ), m i ≠ n i x, y : ι hne : ¬ x = y h : n x = m x ∧ ∀ (x_1 : ι ), x_1 ≠ x m x_1 = update m y (n y x_1
exact ( hm x h : n x = m x ∧ ∀ (x_1 : ι ), x_1 ≠ x m x_1 = update m y (n y x_1 h . 1 : ∀ {a b : Prop }, a ∧ b a . symm : ∀ {α : Sort ?u.6284} {a b : α }, a = b b = a symm ). elim
#align pi.infinite_of_left Pi.infinite_of_left
/-- If at least one `π i` is infinite and the rest nonempty, the pi type of all `π` is infinite. -/
theorem Pi.infinite_of_exists_right { ι : Type _ } { π : ι → Type _ } ( i : ι ) [ Infinite <| π i ]
[∀ i , Nonempty <| π i ] : Infinite (∀ i : ι , π i ) :=
let ⟨ m ⟩ := @ Pi.Nonempty ι π _
Infinite.of_injective _ ( update_injective m i )
#align pi.infinite_of_exists_right Pi.infinite_of_exists_right
/-- See `Pi.infinite_of_exists_right` for the case that only one `π i` is infinite. -/
instance Pi.infinite_of_right { ι : Sort _ } { π : ι → Sort _ } [∀ i , Infinite <| π i ] [ Nonempty ι ] :
Infinite (∀ i : ι , π i ) :=
Pi.infinite_of_exists_right : ∀ {ι : Type ?u.6768} {π : ι → Type ?u.6769i : ι ) [inst : Infinite (π i inst : ∀ (i : ι ), Nonempty (π i ],
Infinite ((i : ι ) → π i ) ( Classical.arbitrary : (α : Sort ?u.6776) → [h : Nonempty α α ι )
#align pi.infinite_of_right Pi.infinite_of_right
/-- Non-dependent version of `Pi.infinite_of_left`. -/
instance Function.infinite_of_left { ι π : Sort _ } [ Nontrivial π ] [ Infinite ι ] : Infinite ( ι → π ) :=
Pi.infinite_of_left
#align function.infinite_of_left Function.infinite_of_left
/-- Non-dependent version of `Pi.infinite_of_exists_right` and `Pi.infinite_of_right`. -/
instance Function.infinite_of_right { ι π : Sort _ } [ Infinite π ] [ Nonempty ι ] : Infinite ( ι → π ) :=
Pi.infinite_of_right
#align function.infinite_of_right Function.infinite_of_right
end