# Zulip Chat Archive

## Stream: new members

### Topic: subsets

#### Leonid Kimelfeld (Feb 24 2021 at 16:19):

Hi!

in nice workshop by Kevin Buzzard there is example:

lemma subset_def : X ⊆ Y ↔ ∀ a, a ∈ X → a ∈ Y :=

begin

refl

end

I see the definition of notations ⊆ and ∈. But I can't understand why above lemma is by definition?

#### Kenny Lau (Feb 24 2021 at 16:22):

#### Kenny Lau (Feb 24 2021 at 16:22):

how is `X ⊆ Y`

defined?

#### Leonid Kimelfeld (Feb 24 2021 at 16:36):

there is declaration:

"variables (Ω : Type) (X Y : set Ω)"

I see (notation) that

⊆ is "has_subset.subset : Π {α : Type} [c : has_subset α], α → α → Prop"

∈ is "has_mem.mem : Π {α γ : Type} [c : has_mem α γ], α → γ → Prop"

#### Alex J. Best (Feb 24 2021 at 16:45):

@Leonid Kimelfeld it will be easier to understand your questions if you give a #mwe (including the definitions of what X and Y are).

But assuming that they are sets: `⊆`

means `has_subset.subset`

as you say, but the definition of `has_subset`

for `set`

defines this as docs#set.subset which is

```
protected def subset (s₁ s₂ : set α) :=
∀ ⦃a⦄, a ∈ s₁ → a ∈ s₂
```

which is exactly the right hand side of your iff, so this is true by definition.

#### Alex J. Best (Feb 24 2021 at 16:46):

By using the infoview in vscode you can click on `X ⊆ Y`

to see that the term is defined in terms of `set.has_subset`

which you can look up.

#### Leonid Kimelfeld (Feb 24 2021 at 17:07):

thank you, now it seems clear

Last updated: May 06 2021 at 21:09 UTC