From 3d637cea4a4e45f51bc88a2f09ef38fd72618fb7 Mon Sep 17 00:00:00 2001 From: Moritz Firsching Date: Sun, 6 Oct 2024 20:06:17 +0000 Subject: [PATCH] chore(Order/Heyting/Hom): remove left-over TODO (#17475) This is already present. Co-authored-by: Moritz Firsching --- Mathlib/Order/Heyting/Hom.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Order/Heyting/Hom.lean b/Mathlib/Order/Heyting/Hom.lean index 358a7b6215806..6b0940817f6d3 100644 --- a/Mathlib/Order/Heyting/Hom.lean +++ b/Mathlib/Order/Heyting/Hom.lean @@ -190,7 +190,6 @@ theorem map_compl (a : α) : f aᶜ = (f a)ᶜ := by rw [← himp_bot, ← himp_ @[simp] theorem map_bihimp (a b : α) : f (a ⇔ b) = f a ⇔ f b := by simp_rw [bihimp, map_inf, map_himp] --- TODO: `map_bihimp` end HeytingAlgebra section CoheytingAlgebra