import Mathlib.Data.Set.Basic
open Set

variable {α : Type}
variable (s t : Set α)

example : (s \\setminus t) ∪ t = s ∪ t :=
by sorry

import Mathlib.Data.Set.Basic
open Set
variable {α : Type}
variable (s t : Set α)

example : s ∪ (s ∩ t) = s :=
by sorry

import Mathlib.Data.Set.Basic
open Set
variable {α : Type}
variable (s t : Set α)

example : s ∩ t = t ∩ s :=
by sorry

import Mathlib.Data.Set.Basic
open Set
variable {α : Type}
variable (s t u : Set α)

example : s \ (t ∪ u) ⊆ (s \ t) \ u :=
by sorry

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set

variable {α : Type}
variable (s t u : Set α)

example : (s ∩ t) ∪ (s ∩ u) ⊆ s ∩ (t ∪ u):=
by sorry

import Mathlib.Data.Set.Basic
import Mathlib.Tactic

open Set
variable {α : Type}
variable (s t u : Set α)

example : (s \ t) \ u ⊆ s \ (t ∪ u) :=
by sorry

import Mathlib.Data.Set.Basic
import Mathlib.Tactic
open Set
variable {α : Type}
variable (s t u : Set α)

example :
  s ∩ (t ∪ u) ⊆ (s ∩ t) ∪ (s ∩ u) :=
by sorry

import Mathlib.Data.Set.Basic
import Mathlib.Tactic
open Set
variable {α : Type}
variable (s t u : Set α)

example
  (h : s ⊆ t)
  : s ∩ u ⊆ t ∩ u :=
by sorry

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (u v w : ℕ → ℝ)
variable (a : ℝ)

def limite : (ℕ → ℝ) → ℝ → Prop :=
  fun u c ↦ ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - c| ≤ ε

example
  (hu : limite u a)
  (hw : limite w a)
  (h1 : ∀ n, u n ≤ v n)
  (h2 : ∀ n, v n ≤ w n) :
  limite v a :=
by sorry

import Mathlib.Data.Set.Basic
import Mathlib.Tactic
open Set
variable {α : Type}
variable (s t : Set α)

example : s ∩ (s ∪ t) = s :=
by sorry