subsets

Stream: new members

[Leonid Kimelfeld]

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]

#backticks

[Kenny Lau]

how is X ⊆ Y defined?

[Leonid Kimelfeld]

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]

@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]

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]

thank you, now it seems clear