Type of sets containing a given set

Stream: new members

[Thomas Browning]

Is there a name in mathlib for the Type of sets containing a given set?

[Kevin Buzzard]

You could use Icc but there might be a better way.

[Pedro Minicz]

Something like this could work:

variables {α : Type} {s : set α}

def subset : Type := {t // s ⊆ t}

[Kevin Buzzard]

Right -- the question is whether it's already there (in which case it might have an API)

[Kevin Buzzard]

What do you want to do with it?

[Thomas Browning]

establish a galois connection between (subsets of L containing K) and (intermediate fields of L/K)

[Thomas Browning]

actually, it's possible that I don't need to insist that the subset contains K in order for this to work

[Kevin Buzzard]

If you just use subsets is it not a Galois connection?

[Kevin Buzzard]

yeah, what you said

[Reid Barton]

I think you don't need to include "containing K" to get a Galois connection, yeah

[Kevin Buzzard]

It might even be a Galois insertion? The subfield generated by a subfield is itself.

[Thomas Browning]

yeah, might be