Commit 2023-01-14 13:55 38edbb8f

View on Github →

feat: port Logic.Encodable.Lattice (#1571)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Logic/Encodable/Lattice.lean

added theorem Encodable.supᵢ_decode₂

added theorem Encodable.unionᵢ_decode₂

added theorem Encodable.unionᵢ_decode₂_cases

added theorem Encodable.unionᵢ_decode₂_disjoint_on