Properties of relative upper/lower sets #

This file proves results on IsRelUpperSet and IsRelLowerSet.

source

@[simp]

theorem isRelUpperSet_true_iff_isUpperSet {α : Type u_1} {s : Set α} [LE α] :

(IsRelUpperSet s fun (x : α) => True) ↔ IsUpperSet s

source

@[simp]

theorem isRelLowerSet_true_iff_isLowerSet {α : Type u_1} {s : Set α} [LE α] :

(IsRelLowerSet s fun (x : α) => True) ↔ IsLowerSet s

source

theorem IsUpperSet.isRelUpperSet_sep {α : Type u_1} {s : Set α} (P : α → Prop) [LE α] (hs : IsUpperSet s) :

IsRelUpperSet {x : α | x ∈ s ∧ P x} P

source

theorem IsLowerSet.isRelLowerSet_sep {α : Type u_1} {s : Set α} (P : α → Prop) [LE α] (hs : IsLowerSet s) :

IsRelLowerSet {x : α | x ∈ s ∧ P x} P

source

theorem IsRelLowerSet.mono_isLowerSet {α : Type u_1} {s t : Set α} {P : α → Prop} [LE α] (ht : IsRelLowerSet t P) (hs : IsLowerSet s) (hst : s ⊆ t) :

IsRelLowerSet s P

A subset that is a lower set is additionally a relative lower set.

source

theorem IsRelUpperSet.mono_isUpperSet {α : Type u_1} {s t : Set α} {P : α → Prop} [LE α] (ht : IsRelUpperSet t P) (hs : IsUpperSet s) (hst : s ⊆ t) :

IsRelUpperSet s P

A subset that is an upper set is additionally a relative upper set.

source

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

P a

source

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

P a

source

theorem IsRelUpperSet.mem_of_le {α : Type u_1} {s : Set α} {a b : α} {P : α → Prop} [LE α] (hs : IsRelUpperSet s P) (h : a ∈ s) (h₁ : a ≤ b) (h₂ : P b) :

b ∈ s

source

theorem IsRelLowerSet.mem_of_le {α : Type u_1} {s : Set α} {a b : α} {P : α → Prop} [LE α] (hs : IsRelLowerSet s P) (h : a ∈ s) (h₁ : b ≤ a) (h₂ : P b) :

b ∈ s

source

@[simp]

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

IsRelUpperSet ∅ P

source

@[simp]

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

IsRelLowerSet ∅ P

source

@[simp]

theorem isRelUpperSet_self {α : Type u_1} {s : Set α} [LE α] :

IsRelUpperSet s fun (x : α) => x ∈ s

source

@[simp]

theorem isRelLowerSet_self {α : Type u_1} {s : Set α} [LE α] :

IsRelLowerSet s fun (x : α) => x ∈ s

source

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

IsRelUpperSet (s ∪ t) P

source

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

IsRelLowerSet (s ∪ t) P

source

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

IsRelUpperSet (s ∩ t) P

source

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

IsRelLowerSet (s ∩ t) P

source

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

IsRelUpperSet (⋃₀ S) P

source

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

IsRelLowerSet (⋃₀ S) P

source

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

source

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

source

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

source

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

source

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

IsRelUpperSet (⋂₀ S) P

source

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

IsRelLowerSet (⋂₀ S) P

source

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

source

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

source

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

source

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) :