LowerSet of a LowerSet

Stream: Is there code for X?

[Pedro Sánchez Terraf]

Do we have the result that a docs#LowerSet of LowerSet is a LowerSet of the ambient type?

import Mathlib.Data.Set.Functor
import Mathlib.Order.UpperLower.Basic

namespace LowerSet

open Set

/--
The relation of being a lower-set is transitive.
-/
lemma IsLowerSet_of_IsLowerSet [Preorder α] {C : Set α} {S : Set C} (hC : IsLowerSet C)
    (hS : IsLowerSet S) : IsLowerSet (S : Set α) := by
  rintro _ b b_le_a ⟨a,a_in_S,rfl⟩
  exact mem_image_val_of_mem (hC b_le_a a.property) (hS b_le_a a_in_S)

/--
Lifting a lower-set from inside another.
-/
def lift [Preorder α] (C : LowerSet α) (S : LowerSet C) : LowerSet α :=
  ⟨S.carrier, IsLowerSet_of_IsLowerSet C.lower' S.lower'⟩

Do we want it?

Context: I was trying to use this infrastructure for a mini-project, and I needed these lemmas. It finally happened that I had to work with down-sets qua sets very much, so I ended up defining “C is a down-set of D”, for C D : Set α. But perhaps they come up again.

A second lemma was about “inducing” a LowerSet inside another (have it? want it?):

/--
The trace of a lower-set on any subset is a lower-set.
-/
lemma IsLowerSet_trace [Preorder α] {C S : Set α} (hS : IsLowerSet S) :
    IsLowerSet {c : C | (c : α) ∈ S} :=
    -- Alternate spelling: `IsLowerSet ((↑) ⁻¹' S : Set C)`
  fun ⦃_ _⦄ b_le_a a_in_S => hS b_le_a a_in_S

/--
The trace of a lower-set on a subset.
-/
def trace [Preorder α] {C : Set α} (S : LowerSet α) : LowerSet C :=
  ⟨{c : C | (c : α) ∈ S}, IsLowerSet_trace S.lower'⟩

/--
The trace operation preserves the carrier if already included.
-/
lemma trace_of_subset [Preorder α] {C : Set α} {S : LowerSet α} (sub : S.carrier ⊆ C) :
    (↑) '' ((trace S).carrier : Set C) = S.carrier := by
  calc
    (↑) '' ((trace S).carrier : Set C) = ((↑) '' ((↑) ⁻¹' S.carrier : Set C) : Set α) := rfl
    _ = S.carrier := by rw [Subtype.image_preimage_coe]; simp_all

(Edit: corrected code for latest Mathlib)

[Yaël Dillies]

We don't have them and I don't know whether we want them but we could. Thought needs to be given in whether you want to use IsLowerSet or LowerSet in both places where they appear.

[Emilie (Shad Amethyst)]

Is this not a general property of order embeddings whose image range is a LowerSet?

[Pedro Sánchez Terraf]

Yaël Dillies said:

Thought needs to be given in whether you want to use IsLowerSet or LowerSet in both places where they appear.

I'm not sure what you mean; in my application? Any hints welcome!

[Pedro Sánchez Terraf]

Or, are you saying that I should restrict myself to use either IsLowerSet or LowerSet? I put both because I was trying to API it a little bit.