BourbakiLean2.Function.Prod

def Function.prod {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} (f : α → β) (f' : α' → β') :

α × α' → β × β'

Equations

Function.prod f f' (x_1, y) = (f x_1, f' y)

Instances For

@[simp]

theorem Function.prod_val {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {f : α → β} {f' : α' → β'} {a : α} {a' : α'} :

Function.prod f f' (a, a') = (f a, f' a')

source

@[simp]

theorem Function.prod_image {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {f : α → β} {f' : α' → β'} {x : Set α} {x' : Set α'} :

Function.prod f f' '' x.prod x' = (f '' x).prod (f' '' x')

source

@[simp]

theorem Function.prod_surj_iff {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {f : α → β} {f' : α' → β'} [Nonempty β] [Nonempty β'] :

Function.Surjective (Function.prod f f') ↔ Function.Surjective f ∧ Function.Surjective f'

source

@[simp]

theorem Function.prod_inj_iff {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {f : α → β} {f' : α' → β'} [Nonempty α] [Nonempty α'] :

Function.Injective (Function.prod f f') ↔ Function.Injective f ∧ Function.Injective f'

source

@[simp]

theorem Function.prod_bij_iff {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {f : α → β} {f' : α' → β'} [Nonempty α] [Nonempty α'] [Nonempty β] [Nonempty β'] :

Function.Bijective (Function.prod f f') ↔ Function.Bijective f ∧ Function.Bijective f'

source

theorem Function.comp_prod_comp {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {γ : Type u_5} {γ' : Type u_6} {f : α → β} {f' : α' → β'} {g : γ → α} {g' : γ' → α'} :

Function.prod (f ∘ g) (f' ∘ g') = Function.prod f f' ∘ Function.prod g g'

source

@[simp]

theorem Function.id_prod_id {α : Type u_1} {α' : Type u_2} :

Function.prod id id = id

source

theorem Function.prod_inverse {α : Type u_1} {α' : Type u_2} {β : Type u_3} {β' : Type u_4} {f : α → β} {f' : α' → β'} {g : β → α} {g' : β' → α'} (h : Function.IsInverseOf g f) (h' : Function.IsInverseOf g' f') :

Function.IsInverseOf (Function.prod g g') (Function.prod f f')

source

instance Function.instUniqueForall {x : False → Type u_12} :

Unique ((a : False) → x a)

Equations

Function.instUniqueForall = { default := fun (a : False) => nomatch a, uniq := ⋯ }

source

theorem Function.prod_const {ι : Type u_1} {α : Type u_3} :

((i : ι) → Function.const ι α i) = (ι → α)

source

def Function.prod_unique {ι : Type u_1} {x : ι → Type u_9} [inst : Unique ι] :

Function.Bijection ((i : ι) → x i) (x default)

Equations

Function.prod_unique = Function.bijection_of_funcs (fun (x : (i : ι) → x i) => x default) (fun (a : x default) (i : ι) => ⋯ ▸ a) ⋯ ⋯

Instances For

source

def Function.prod_bool {α β : Type u_3} :

Function.Bijection ((i : Bool) → if i = true then α else β) (α × β)

Equations

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

Instances For

source

theorem Function.nonempty_prod {ι : Type u_1} {x : ι → Type u_9} (h : ∀ (i : ι), Nonempty (x i)) :

Nonempty ((i : ι) → x i)

source

def Function.unique_prod_of_unique {ι : Type u_1} {x : ι → Type u_9} (h : (i : ι) → Unique (x i)) :

Unique ((i : ι) → x i)

Equations

Function.unique_prod_of_unique h = { default := fun (i : ι) => default, uniq := ⋯ }

Instances For

source

@[simp]

theorem Function.const_inj {α : Type u_3} {β : Type u_5} [inst : Nonempty β] :

Function.Injective (Function.const β)

source

def Function.reindex_by_bij {ι : Type u_1} {ι' : Type u_2} {x : ι → Type u_9} (f : Function.Bijection ι' ι) :

Function.Bijection ((i : ι) → x i) ((i' : ι') → x (f.val i'))

Equations

Function.reindex_by_bij f = ⟨fun (h : (i : ι) → x i) (i' : ι') => h (f.val i'), ⋯⟩

Instances For

source

theorem Function.subfamily_covered {ι : Type u_1} {ι' : Type u_2} {x : ι → Type u_9} {f : Function.Injection ι' ι} (h : ∀ (i : ι), Nonempty (x i)) :

Function.Surjective fun (a : (i : ι) → x i) (i' : ι') => a (f.val i')

source

@[simp]

theorem Function.apply_surjective {ι : Type u_1} {x : ι → Type u_9} (h : ∀ (i : ι), Nonempty (x i)) {i : ι} :

Function.Surjective fun (a : (i : ι) → x i) => a i

source

@[simp]

theorem Function.prod_nonempty_iff {ι : Type u_1} {x : ι → Type u_9} :

Nonempty ((i : ι) → x i) ↔ ∀ (i : ι), Nonempty (x i)

source

def Function.prod_map {ι : Type u_1} {x : ι → Type u_9} {y : ι → Type u_10} (f : (i : ι) → x i → y i) (a : (i : ι) → x i) (i : ι) :

y i

Equations

Function.prod_map f a i = f i (a i)

Instances For

source

@[simp]

theorem Function.prod_map_comp {ι : Type u_1} {x : ι → Type u_9} {y : ι → Type u_10} {z : ι → Type u_11} {f : (i : ι) → x i → y i} {g : (i : ι) → z i → x i} :

(Function.prod_map fun (i : ι) (c : z i) => f i (g i c)) = Function.prod_map f ∘ Function.prod_map g

source

@[simp]

theorem Function.prod_map_id {ι : Type u_1} {x : ι → Type u_9} :

(Function.prod_map fun (x_1 : ι) (a : x x_1) => a) = id

source

theorem Function.prod_map_inj {ι : Type u_1} {x : ι → Type u_9} {y : ι → Type u_10} {f : (i : ι) → x i → y i} (h : ∀ (i : ι), Function.Injective (f i)) :

Function.Injective (Function.prod_map f)

source

@[simp]

theorem Function.prod_map_inj_iff {ι : Type u_1} {x : ι → Type u_9} {y : ι → Type u_10} (h : ∀ (i : ι), Nonempty (x i)) {f : (i : ι) → x i → y i} :

Function.Injective (Function.prod_map f) ↔ ∀ (i : ι), Function.Injective (f i)

source

def Function.dep_flip {ι : Type u_1} {α : Type u_3} {x : ι → Type u_9} :

Function.Bijection ((i : ι) → α → x i) (α → (i : ι) → x i)

Equations

Function.dep_flip = Function.bijection_of_funcs (fun (f : (i : ι) → α → x i) (a : α) (i : ι) => f i a) (fun (f : α → (i : ι) → x i) (i : ι) (a : α) => f a i) ⋯ ⋯