Zulip Chat Archive

Stream: new members

Topic: subsets


view this post on Zulip 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?

view this post on Zulip Kenny Lau (Feb 24 2021 at 16:22):

#backticks

view this post on Zulip Kenny Lau (Feb 24 2021 at 16:22):

how is X ⊆ Y defined?

view this post on Zulip 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"

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Leonid Kimelfeld (Feb 24 2021 at 17:07):

thank you, now it seems clear


Last updated: May 06 2021 at 21:09 UTC