mathlib3
daec7d61 - chore(order/bounded_order): Rename `is_complemented` to `complemented_lattice` (#16263)

Commit

3 years ago

chore(order/bounded_order): Rename `is_complemented` to `complemented_lattice` (#16263) This is to make space for the predicate `is_complemented : α → Prop := ∃ b, is_compl a b`.

Author

YaelDillies

Parents

24b08ce6

mathlib3 daec7d61 - chore(order/bounded_order): Rename `is_complemented` to `complemented_lattice` (#16263)

mathlib3
daec7d61 - chore(order/bounded_order): Rename `is_complemented` to `complemented_lattice` (#16263)