michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(lean/tests/lean/run/new_obtain{3,4}): adapt tests to new notation for image

Browse source
This commit is contained in:
Jeremy Avigad 2016-01-03 21:40:56 -05:00 committed by Leonardo de Moura
parent d9118ded76
commit a22346e411
2 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
tests/lean/run/new_obtain3.lean
View file

@ -3,13 +3,13 @@ open set function eq.ops
variables {X Y Z : Type}
lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] :=
lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
ext (take z,
iff.intro
(assume Hz : z ∈ (f ∘ g) '[a],
(assume Hz : z ∈ (f ∘ g) ' a,
obtain x (Hx₁ : x ∈ a) (Hx₂ : f (g x) = z), from Hz,
have Hgx : g x ∈ g '[a], from mem_image Hx₁ rfl,
show z ∈ f '[g '[a]], from mem_image Hgx Hx₂)
(assume Hz : z ∈ f '[g '[a]],
have Hgx : g x ∈ g ' a, from mem_image Hx₁ rfl,
show z ∈ f ' (g ' a), from mem_image Hgx Hx₂)
(assume Hz : z ∈ f ' (g ' a),
obtain y [x (Hz₁ : x ∈ a) (Hz₂ : g x = y)] (Hy₂ : f y = z), from Hz,
show z ∈ (f ∘ g) '[a], from mem_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))
show z ∈ (f ∘ g) ' a, from mem_image Hz₁ (Hz₂⁻¹ ▸ Hy₂)))

2
tests/lean/run/new_obtain4.lean
View file

@ -3,7 +3,7 @@ open set function eq.ops
variables {X Y Z : Type}
lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) '[a] = f '[g '[a]] :=
lemma image_compose (f : Y → X) (g : X → Y) (a : set X) : (f ∘ g) ' a = f ' (g ' a) :=
ext (take z,
iff.intro
(assume Hz,