Imagen de la intersección general mediante inyectiva
Demostrar que si f es inyectiva, entonces
|
1 |
(⋂ i, f[A i]) ⊆ f[⋂ i, A i] |
Para ello, completar la siguiente teoría de Lean:
|
1 2 3 4 5 6 7 8 9 10 11 12 13 14 |
import data.set.basic import tactic open set function variables {α : Type*} {β : Type*} {I : Type*} variable f : α → β variables A : I → set α example (i : I) (injf : injective f) : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) := sorry |
[expand title=»Soluciones con 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 |
import data.set.basic import tactic open set function variables {α : Type*} {β : Type*} {I : Type*} variable f : α → β variables A : I → set α -- 1ª demostración -- =============== example (i : I) (injf : injective f) : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) := begin intros y hy, rw mem_Inter at hy, rcases hy i with ⟨x, xAi, fxy⟩, use x, split, { apply mem_Inter_of_mem, intro j, rcases hy j with ⟨z, zAj, fzy⟩, convert zAj, apply injf, rw fxy, rw ← fzy, }, { exact fxy, }, end -- 2ª demostración -- =============== example (i : I) (injf : injective f) : (⋂ i, f '' A i) ⊆ f '' (⋂ i, A i) := begin intro y, simp, intro h, rcases h i with ⟨x, xAi, fxy⟩, use x, split, { intro j, rcases h j with ⟨z, zAi, fzy⟩, have : f x = f z, by rw [fxy, fzy], have : x = z, from injf this, rw this, exact zAi, }, { exact fxy, }, end |
Se puede interactuar con la prueba anterior en esta sesión con Lean,
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]
[expand title=»Soluciones con Isabelle/HOL»]
|
1 |
En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>
[/expand]