Theorem Set.ite_eq_of_subset_left

Modification history

2025-07-03 15:35

Mathlib/Data/Set/Basic.lean

chore: move `BooleanAlgebra` material on `Set` out of `Data` (#26665) …

Modified Set.ite_eq_of_subset_left View on Github →

2023-10-30 17:26

Mathlib/Data/Set/Basic.lean

Misc lemmas about Specializes, Inseparable and path-connectedness (#7970) …

Added Set.ite_eq_of_subset_left View on Github →