-
Notifications
You must be signed in to change notification settings - Fork 298
/
prod.lean
64 lines (45 loc) · 2.14 KB
/
prod.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl
Extends theory on products
-/
import tactic.ext
universes u v
variables {α : Type u} {β : Type v}
@[simp] theorem prod.forall {p : α × β → Prop} : (∀ x, p x) ↔ (∀ a b, p (a, b)) :=
⟨assume h a b, h (a, b), assume h ⟨a, b⟩, h a b⟩
@[simp] theorem prod.exists {p : α × β → Prop} : (∃ x, p x) ↔ (∃ a b, p (a, b)) :=
⟨assume ⟨⟨a, b⟩, h⟩, ⟨a, b, h⟩, assume ⟨a, b, h⟩, ⟨⟨a, b⟩, h⟩⟩
namespace prod
@[simp] theorem mk.inj_iff {a₁ a₂ : α} {b₁ b₂ : β} : (a₁, b₁) = (a₂, b₂) ↔ (a₁ = a₂ ∧ b₁ = b₂) :=
⟨prod.mk.inj, by cc⟩
lemma ext_iff {p q : α × β} : p = q ↔ p.1 = q.1 ∧ p.2 = q.2 :=
by rw [← @mk.eta _ _ p, ← @mk.eta _ _ q, mk.inj_iff]
@[extensionality]
lemma ext {α β} {p q : α × β} : p.1 = q.1 → p.2 = q.2 → p = q :=
by rw [ext_iff] ; intros ; split ; assumption
/-- Swap the factors of a product. `swap (a, b) = (b, a)` -/
def swap : α × β → β × α := λp, (p.2, p.1)
@[simp] lemma swap_swap : ∀ x : α × β, swap (swap x) = x
| ⟨a, b⟩ := rfl
@[simp] lemma fst_swap {p : α × β} : (swap p).1 = p.2 := rfl
@[simp] lemma snd_swap {p : α × β} : (swap p).2 = p.1 := rfl
@[simp] lemma swap_prod_mk {a : α} {b : β} : swap (a, b) = (b, a) := rfl
@[simp] lemma swap_swap_eq : swap ∘ swap = @id (α × β) :=
funext swap_swap
@[simp] lemma swap_left_inverse : function.left_inverse (@swap α β) swap :=
swap_swap
@[simp] lemma swap_right_inverse : function.right_inverse (@swap α β) swap :=
swap_swap
lemma eq_iff_fst_eq_snd_eq : ∀{p q : α × β}, p = q ↔ (p.1 = q.1 ∧ p.2 = q.2)
| ⟨p₁, p₂⟩ ⟨q₁, q₂⟩ := by simp
theorem lex_def (r : α → α → Prop) (s : β → β → Prop)
{p q : α × β} : prod.lex r s p q ↔ r p.1 q.1 ∨ p.1 = q.1 ∧ s p.2 q.2 :=
⟨λ h, by cases h; simp *,
λ h, match p, q, h with
| (a, b), (c, d), or.inl h := lex.left _ _ _ h
| (a, b), (c, d), or.inr ⟨e, h⟩ :=
by change a = c at e; subst e; exact lex.right _ _ h
end⟩
end prod