Verwenden von Sets in Lean

Question

Ich möchte in der Topologie mit Lean arbeiten.

Als guten Anfang wollte ich ein paar einfache Lemmas über sets in lean beweisen.

Zum Beispiel

def inter_to_union (H : a ∈ set.inter A B) : a ∈ set.union A B := 
    sorry 

oder

def set_deMorgan : a ∈ set.inter A B → a ∈ set.compl (set.union (set.compl A) (set.compl B)) := 
sorry 

oder vielleicht noch interessanter ist

def set_deMorgan2 : set.inter A B = set.compl (set.union (set.compl A) (set.compl B)) := 
sorry 

Aber ich kann nicht überall Beseitigungsregeln für set.union oder set.inter, so dass ich nur finden Ich weiß nicht, wie ich mit ihnen arbeiten soll.

1. Wie beweise ich die Lemmas?

Auch am definition of sets in lean suche, kann ich Bits Syntax sehen, die wie Papier Mathematik sehr viel aussehen, aber ich weiß nicht auf der Ebene der abhängigen Typ Theorie, zum Beispiel verstehen:

protected def sep (p : α → Prop) (s : set α) : set α := 
{a | a ∈ s ∧ p a} 

2. Wie kann man das obige Beispiel in einfachere Begriffe von abhängigen/induktiven Typen aufteilen?

   def set (α : Type u) := α → Prop 
   

   Wenn Sie einen Satz s : set α und Sie s a, diese nachweisen können, für einige x : α haben:

Answer 1

Das Modul (in der Regel ‚das Universum‘ genannt wird α) Sätze mit Prädikaten auf irgendeine Art α identifiziert wird interpretiert als 'x gehört zu s'.

In diesem Fall ist x ∈ A eine Notation (lassen Sie uns über typeclasses jetzt nichts dagegen) für set.mem x A, die wie folgt definiert ist:

protected def mem (a : α) (s : set α) := 
s a 

Die oben erklärt, warum die leere Menge als Prädikat dargestellt wird immer false Rückkehr:

instance : has_emptyc (set α) := 
⟨λ a, false⟩ 

Und auch das Universum wenig überraschend wie so dargestellt:

def univ : set α := 
λ a, true 

Ich werde zeigen, wie das erste Lemma beweisen:

def inter_to_union {α : Type} {A B : set α} {a : α} : A ∩ B ⊆ A ∪ B := 
    assume (x : α) (xinAB : x ∈ A ∩ B),  -- unfold the definition of `subset` 
    have xinA : x ∈ A, from and.left xinAB, 
    @or.inl _ (x ∈ B) xinA 

Das alles wie die üblichen „pointful“ Beweise für diese Eigenschaften in Basis-Set-Theorie ist.

In Bezug auf Ihre Frage zu sep - Sie können wie so durch Notationen siehe:

set_option pp.notation false 
#print set.sep 

ist hier die Ausgabe:

protected def set.sep : Π {α : Type u}, (α → Prop) → set α → set α := 
λ {α : Type u} (p : α → Prop) (s : set α), 
    set_of (λ (a : α), and (has_mem.mem a s) (p a))