Revision #2376 → #3025 · back to history
modifiedProper subset1b5d0d5297f7
| Field | From #2376 | To #3025 |
|---|
| note | Set's `⊂` (HasSSubset, characterized by ssubset_def) is proper subset: `s ⊆ t ∧ ¬t ⊆ s`. | Set.ssubset_def characterizes `s ⊂ t` as `s ⊆ t ∧ ¬t ⊆ s`, the proper-subset relation. |
modified⊂ / ⊃ as proper subset / superset35caef8f3347
| Field | From #2376 | To #3025 |
|---|
| mathlib.decl | Set.instHasSSubset | Set.ssubset_def |
| note | Mathlib follows this convention: `⊂` (Set.instHasSSubset) denotes proper subset, defined as `<`. | Mathlib follows this convention: on `Set α`, `⊂` denotes proper subset (Set.ssubset_def unfolds it to `s ⊆ t ∧ ¬t ⊆ s`). |
modifiedInclusion is the canonical partial orderd6f9505906f3
| Field | From #2376 | To #3025 |
|---|
| mathlib.decl | Set.instBooleanAlgebra | Set.le_eq_subset |
| mathlib.match_kind | generalization | exact |
| mathlib.module | Mathlib.Order.BooleanAlgebra.Set | Mathlib.Data.Set.Basic |
| note | The canonical `≤` on `Set α` is inclusion (Set.le_eq_subset), provided by its BooleanAlgebra/partial-order structure. | Set.le_eq_subset proves the canonical `≤` on `Set α` is exactly `⊆`. |