Order theoretic results

theorem csupr_neg {α : Type u_1} [CompleteLattice α] {p : Prop} {f : p → α} (hp : ¬p) : ⨆ (h : p), f h = ⊥

@[simp]

theorem Set.compl_eq_empty {α : Type u_1} {s : Set α} : sᶜ = ∅ ↔ s = Set.univ

@[simp]

theorem Set.compl_eq_univ {α : Type u_1} {s : Set α} : sᶜ = Set.univ ↔ s = ∅

@[simp]

theorem Set.iUnion_pos {α : Type u_1} {p : Prop} {f : p → Set α} (hp : p) : ⋃ (h : p), f h = f hp

@[simp]

theorem Set.iUnion_neg' {α : Type u_1} {p : Prop} {f : p → Set α} (hp : ¬p) : ⋃ (h : p), f h = ∅

@[simp]

theorem Set.empty_symmDiff {α : Type u_1} (s : Set α) : symmDiff ∅ s = s

@[simp]

theorem Set.symmDiff_empty {α : Type u_1} (s : Set α) : symmDiff s ∅ = s