José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ f⁻¹[v] ⊆ f⁻¹[f[s] ∪ v]". <a href="https://jaalonso.github.io/calculemus/posts/2025/04/25-union_con_la_imagen_inversa" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2025/04/25-union_con_la_imagen_inversa</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
mastodon.online is one of the many independent Mastodon servers you can use to participate in the fediverse.
A newer server operated by the Mastodon gGmbH non-profit
Administered by:
Server stats:
10Kactive users
mastodon.online: About · Status · Profiles directory · Privacy policy
Mastodon: About · Get the app · Keyboard shortcuts · View source code · v4.4.0-nightly.2025-04-28
#Calculemus
4 posts · 4 participants · 0 posts today
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] ∩ v = f[s ∩ f⁻¹[v]]". <a href="https://jaalonso.github.io/calculemus/posts/2025/04/24-interseccion_con_la_imagen_inversa/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2025/04/24-interseccion_con_la_imagen_inversa/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "f[s ∪ f⁻¹[v]] ⊆ f[s] ∪ v". <a href="https://jaalonso.github.io/calculemus/posts/2025/04/23-union_con_la_imagen/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2025/04/23-union_con_la_imagen/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] ∩ t = f[s ∩ f⁻¹[t]]". <a href="https://jaalonso.github.io/calculemus/posts/2025/04/22-interseccion_con_la_imagen/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2025/04/22-interseccion_con_la_imagen/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "f[s] \ f[t] ⊆ f[s \ t]". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/17-imagen_de_la_diferencia_de_conjuntos/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/17-imagen_de_la_diferencia_de_conjuntos/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es inyectiva, entonces f[s] ∩ f[t] ⊆ f[s ∩ t]". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/16-imagen_de_la_interseccion_de_aplicaciones_inyectivas/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/16-imagen_de_la_interseccion_de_aplicaciones_inyectivas/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "f[s ∩ t] ⊆ f[s] ∩ f[t]". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/15-imagen_de_la_interseccion/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/15-imagen_de_la_interseccion/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "f⁻¹[A ∪ B] = f⁻¹[A] ∪ f⁻¹[B]". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/14-imagen_inversa_de_la_union/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/14-imagen_inversa_de_la_union/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "Si u ⊆ v, entonces f⁻¹[u] ⊆ f⁻¹[v]". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/13-monotonia_de_la_imagen_inversa/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/13-monotonia_de_la_imagen_inversa/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "Monotonía de la imagen de conjuntos". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/12-monotonia_de_la_imagen_de_conjuntos/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/12-monotonia_de_la_imagen_de_conjuntos/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es suprayectiva, entonces u ⊆ f[f⁻¹[u]]". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/11-imagen_de_imagen_inversa_de_aplicaciones_suprayectivas/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/11-imagen_de_imagen_inversa_de_aplicaciones_suprayectivas/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "f[f⁻¹[u]] ⊆ u". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/10-imagen_de_la_imagen_inversa/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/10-imagen_de_la_imagen_inversa/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p><a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a>: Demostraciones con Lean4 y con Isabelle/HOL de "Si f es inyectiva, entonces f⁻¹[f[s]] ⊆ s". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/09-imagen_inversa_de_la_imagen_de_aplicaciones_inyectivas/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/09-imagen_inversa_de_la_imagen_de_aplicaciones_inyectivas/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a></p>
José A. Alonso<p>Demostraciones con Lean4 y con Isabelle/HOL de "f(s) ⊆ u ↔ s ⊆ f⁻¹(u)". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/08-subconjunto_de_la_imagen_inversa/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/08-subconjunto_de_la_imagen_inversa/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a></p>
José A. Alonso<p>Demostraciones con Lean4 y con Isabelle/HOL de "s ⊆ f⁻¹(f(s))". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/07-imagen_inversa_de_la_imagen/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/07-imagen_inversa_de_la_imagen/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a></p>
José A. Alonso<p>Demostraciones con Lean4 y con Isabelle/HOL de "f(s ∪ t) = f(s) ∪ f(t)". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/06-imagen_de_la_union/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/06-imagen_de_la_union/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a></p>
José A. Alonso<p>Demostraciones con Lean4 y con Isabelle/HOL de "f⁻¹(u ∩ v) = f⁻¹(u) ∩ f⁻¹(v)". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/05-imagen_inversa_de_la_interseccion/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/05-imagen_inversa_de_la_interseccion/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a></p>
José A. Alonso<p>Demostraciones con Lean4 y con Isabelle/HOL de "s ∪ (⋂ i, A i) = ⋂ i, (A i ∪ s)". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/04-union_con_interseccion_general/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/04-union_con_interseccion_general/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a></p>
José A. Alonso<p>Demostraciones con Lean4 y con Isabelle/HOL de "⋂_i, (A(i) ∩ B(i)) = (⋂_i, A(i)) ∩ (⋂_i, B(i))". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/03-interseccion_de_intersecciones/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/03-interseccion_de_intersecciones/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a></p>
José A. Alonso<p>Demostraciones con Lean4 y con Isabelle/HOL de "s ∩ ⋃_i A(i) = ⋃_i (A(i) ∩ s)". <a href="https://jaalonso.github.io/calculemus/posts/2021/06/02-distributiva_de_la_interseccion_respecto_de_la_union_general/" rel="nofollow noopener" translate="no" target="_blank"><span class="invisible">https://</span><span class="ellipsis">jaalonso.github.io/calculemus/</span><span class="invisible">posts/2021/06/02-distributiva_de_la_interseccion_respecto_de_la_union_general/</span></a> <a href="https://mathstodon.xyz/tags/LeanProver" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>LeanProver</span></a> <a href="https://mathstodon.xyz/tags/IsabelleHOL" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>IsabelleHOL</span></a> <a href="https://mathstodon.xyz/tags/Math" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Math</span></a> <a href="https://mathstodon.xyz/tags/Calculemus" class="mention hashtag" rel="nofollow noopener" target="_blank">#<span>Calculemus</span></a></p>
ExploreLive feeds
Mastodon is the best way to keep up with what's happening.
Follow anyone across the fediverse and see it all in chronological order. No algorithms, ads, or clickbait in sight.
LoginDrag & drop to upload