Properties of relative upper/lower sets

This file proves results on IsRelUpperSet and IsRelLowerSet.

theorem IsRelUpperSet.prop_of_mem {α : Type u_1} {s : Set α} {a : α} {P : α → Prop} [LE α] (hs : IsRelUpperSet s P) (h : a ∈ s) : P a

theorem IsRelLowerSet.prop_of_mem {α : Type u_1} {s : Set α} {a : α} {P : α → Prop} [LE α] (hs : IsRelLowerSet s P) (h : a ∈ s) : P a

@[simp]

theorem isRelUpperSet_empty {α : Type u_1} {P : α → Prop} [LE α] : IsRelUpperSet ∅ P

@[simp]

theorem isRelLowerSet_empty {α : Type u_1} {P : α → Prop} [LE α] : IsRelLowerSet ∅ P

@[simp]

theorem isRelUpperSet_self {α : Type u_1} {s : Set α} [LE α] : IsRelUpperSet s fun (x : α) => x ∈ s

@[simp]

theorem isRelLowerSet_self {α : Type u_1} {s : Set α} [LE α] : IsRelLowerSet s fun (x : α) => x ∈ s

theorem IsRelUpperSet.union {α : Type u_1} {s t : Set α} {P : α → Prop} [LE α] (hs : IsRelUpperSet s P) (ht : IsRelUpperSet t P) : IsRelUpperSet (s ∪ t) P

theorem IsRelLowerSet.union {α : Type u_1} {s t : Set α} {P : α → Prop} [LE α] (hs : IsRelLowerSet s P) (ht : IsRelLowerSet t P) : IsRelLowerSet (s ∪ t) P

theorem IsRelUpperSet.inter {α : Type u_1} {s t : Set α} {P : α → Prop} [LE α] (hs : IsRelUpperSet s P) (ht : IsRelUpperSet t P) : IsRelUpperSet (s ∩ t) P

theorem IsRelLowerSet.inter {α : Type u_1} {s t : Set α} {P : α → Prop} [LE α] (hs : IsRelLowerSet s P) (ht : IsRelLowerSet t P) : IsRelLowerSet (s ∩ t) P

theorem IsRelUpperSet.sUnion {α : Type u_1} {P : α → Prop} [LE α] {S : Set (Set α)} (hS : ∀ s ∈ S, IsRelUpperSet s P) : IsRelUpperSet (⋃₀ S) P

theorem IsRelLowerSet.sUnion {α : Type u_1} {P : α → Prop} [LE α] {S : Set (Set α)} (hS : ∀ s ∈ S, IsRelLowerSet s P) : IsRelLowerSet (⋃₀ S) P

theorem IsRelUpperSet.iUnion {α : Type u_1} {ι : Sort u_2} {P : α → Prop} [LE α] {f : ι → Set α} (hf : ∀ (i : ι), IsRelUpperSet (f i) P) : IsRelUpperSet (⋃ (i : ι), f i) P

theorem IsRelLowerSet.iUnion {α : Type u_1} {ι : Sort u_2} {P : α → Prop} [LE α] {f : ι → Set α} (hf : ∀ (i : ι), IsRelLowerSet (f i) P) : IsRelLowerSet (⋃ (i : ι), f i) P

theorem IsRelUpperSet.iUnion₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {P : α → Prop} [LE α] {f : (i : ι) → κ i → Set α} (hf : ∀ (i : ι) (j : κ i), IsRelUpperSet (f i j) P) : IsRelUpperSet (⋃ (i : ι), ⋃ (j : κ i), f i j) P

theorem IsRelLowerSet.iUnion₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {P : α → Prop} [LE α] {f : (i : ι) → κ i → Set α} (hf : ∀ (i : ι) (j : κ i), IsRelLowerSet (f i j) P) : IsRelLowerSet (⋃ (i : ι), ⋃ (j : κ i), f i j) P

theorem IsRelUpperSet.sInter {α : Type u_1} {P : α → Prop} [LE α] {S : Set (Set α)} (hS : S.Nonempty) (hf : ∀ s ∈ S, IsRelUpperSet s P) : IsRelUpperSet (⋂₀ S) P

theorem IsRelLowerSet.sInter {α : Type u_1} {P : α → Prop} [LE α] {S : Set (Set α)} (hS : S.Nonempty) (hf : ∀ s ∈ S, IsRelLowerSet s P) : IsRelLowerSet (⋂₀ S) P

theorem IsRelUpperSet.iInter {α : Type u_1} {ι : Sort u_2} {P : α → Prop} [LE α] [Nonempty ι] {f : ι → Set α} (hf : ∀ (i : ι), IsRelUpperSet (f i) P) : IsRelUpperSet (⋂ (i : ι), f i) P

theorem IsRelLowerSet.iInter {α : Type u_1} {ι : Sort u_2} {P : α → Prop} [LE α] [Nonempty ι] {f : ι → Set α} (hf : ∀ (i : ι), IsRelLowerSet (f i) P) : IsRelLowerSet (⋂ (i : ι), f i) P

theorem IsRelUpperSet.iInter₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {P : α → Prop} [LE α] [Nonempty ι] [∀ (i : ι), Nonempty (κ i)] {f : (i : ι) → κ i → Set α} (hf : ∀ (i : ι) (j : κ i), IsRelUpperSet (f i j) P) : IsRelUpperSet (⋂ (i : ι), ⋂ (j : κ i), f i j) P

theorem IsRelLowerSet.iInter₂ {α : Type u_1} {ι : Sort u_2} {κ : ι → Sort u_3} {P : α → Prop} [LE α] [Nonempty ι] [∀ (i : ι), Nonempty (κ i)] {f : (i : ι) → κ i → Set α} (hf : ∀ (i : ι) (j : κ i), IsRelLowerSet (f i j) P) : IsRelLowerSet (⋂ (i : ι), ⋂ (j : κ i), f i j) P

theorem isUpperSet_subtype_iff_isRelUpperSet {α : Type u_1} {P : α → Prop} [LE α] {s : Set { x : α // P x }} : IsUpperSet s ↔ IsRelUpperSet (Subtype.val '' s) P

theorem isLowerSet_subtype_iff_isRelLowerSet {α : Type u_1} {P : α → Prop} [LE α] {s : Set { x : α // P x }} : IsLowerSet s ↔ IsRelLowerSet (Subtype.val '' s) P

instance instSetLikeRelUpperSet {α : Type u_1} {P : α → Prop} [LE α] : SetLike (RelUpperSet P) α

Equations

• instSetLikeRelUpperSet = { coe := RelUpperSet.carrier, coe_injective' := ⋯ }

instance instSetLikeRelLowerSet {α : Type u_1} {P : α → Prop} [LE α] : SetLike (RelLowerSet P) α

Equations

• instSetLikeRelLowerSet = { coe := RelLowerSet.carrier, coe_injective' := ⋯ }

theorem RelUpperSet.isRelUpperSet {α : Type u_1} {P : α → Prop} [LE α] (u : RelUpperSet P) : IsRelUpperSet (↑u) P

theorem RelLowerSet.isRelLowerSet {α : Type u_1} {P : α → Prop} [LE α] (l : RelLowerSet P) : IsRelLowerSet (↑l) P

theorem isRelUpperSet_Icc_le {α : Type u_1} {a : α} [Preorder α] {c : α} : IsRelUpperSet (Set.Icc a c) fun (x : α) => x ≤ c

theorem isRelLowerSet_Icc_ge {α : Type u_1} {a : α} [Preorder α] {c : α} : IsRelLowerSet (Set.Icc c a) fun (x : α) => c ≤ x