Properties of relative upper/lower sets #
This file proves results on IsRelUpperSet and IsRelLowerSet.
@[simp]
theorem
isRelUpperSet_true_iff_isUpperSet
{α : Type u_1}
{s : Set α}
[LE α]
:
(IsRelUpperSet s fun (x : α) => True) ↔ IsUpperSet s
@[simp]
theorem
isRelLowerSet_true_iff_isLowerSet
{α : Type u_1}
{s : Set α}
[LE α]
:
(IsRelLowerSet s fun (x : α) => True) ↔ IsLowerSet s
theorem
IsUpperSet.isRelUpperSet_sep
{α : Type u_1}
{s : Set α}
(P : α → Prop)
[LE α]
(hs : IsUpperSet s)
:
IsRelUpperSet {x : α | x ∈ s ∧ P x} P
theorem
IsLowerSet.isRelLowerSet_sep
{α : Type u_1}
{s : Set α}
(P : α → Prop)
[LE α]
(hs : IsLowerSet s)
:
IsRelLowerSet {x : α | x ∈ s ∧ P x} P
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.
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.
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
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
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
@[simp]
@[simp]
@[simp]
@[simp]
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
@[implicit_reducible]
@[implicit_reducible]
@[implicit_reducible]
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