Skip to content

Commit

Permalink
chore(Order/Heyting/Hom): remove left-over TODO (#17475)
Browse files Browse the repository at this point in the history
This is already present.



Co-authored-by: Moritz Firsching <[email protected]>
  • Loading branch information
mo271 and mo271 committed Oct 6, 2024
1 parent 54d30b7 commit 3d637ce
Showing 1 changed file with 0 additions and 1 deletion.
1 change: 0 additions & 1 deletion Mathlib/Order/Heyting/Hom.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down

0 comments on commit 3d637ce

Please sign in to comment.