Extra facts about prod
#
This file defines prod.swap : α × β → β × α
and proves various simple lemmas about prod
.
@[simp]
@[simp]
@[simp]
theorem
prod.map_mk
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
(f : α → γ)
(g : β → δ)
(a : α)
(b : β) :
theorem
prod.map_comp_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{ε : Type u_5}
{ζ : Type u_6}
(f : α → β)
(f' : γ → δ)
(g : β → ε)
(g' : δ → ζ) :
Composing a prod.map
with another prod.map
is equal to
a single prod.map
of composed functions.
theorem
prod.map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{ε : Type u_5}
{ζ : Type u_6}
(f : α → β)
(f' : γ → δ)
(g : β → ε)
(g' : δ → ζ)
(x : α × γ) :
Composing a prod.map
with another prod.map
is equal to
a single prod.map
of composed functions, fully applied.
theorem
prod.mk.inj_right
{α : Type u_1}
{β : Type u_2}
(b : β) :
function.injective (λ (a : α), (a, b))
@[simp]
@[simp]
@[simp]
@[protected, instance]
def
prod.lex.decidable
{α : Type u_1}
{β : Type u_2}
[decidable_eq α]
(r : α → α → Prop)
(s : β → β → Prop)
[decidable_rel r]
[decidable_rel s] :
decidable_rel (prod.lex r s)
Equations
- prod.lex.decidable r s = λ (p q : α × β), decidable_of_decidable_of_iff or.decidable _
theorem
function.injective.prod_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{f : α → γ}
{g : β → δ}
(hf : function.injective f)
(hg : function.injective g) :
function.injective (prod.map f g)
theorem
function.surjective.prod_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{δ : Type u_4}
{f : α → γ}
{g : β → δ}
(hf : function.surjective f)
(hg : function.surjective g) :
function.surjective (prod.map f g)