LeanPool.AFormalizationOfBorelDeterminacyInLean.Basic.General #

Auxiliary declarations for the Borel determinacy formalization.

@[simp]

theorem Nat.add_div' (k m n : ℕ) (h : n < k) :

(k * m + n) / k = m

@[simp]

theorem Nat.add_sub_sub_of_le {m n p : ℕ} (mn : m ≤ n) (np : n ≤ p) :

n - m + (p - n) = p - m

@[simp]

theorem div_add_self (n : ℕ) :

(n + n) % 2 = 0

theorem Set.hEq_of_image_eq {α : Type u_6} {A A' : Set α} (h : A = A') {B : Set ↑A} {B' : Set ↑A'} (h' : Subtype.val '' B = Subtype.val '' B') :

B ≍ B'

theorem exists_exists_and_eq {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Prop} :

(∃ (b : β), p b ∧ ∃ (a : α), b = f a) ↔ ∃ (a : α), p (f a)

theorem exists_exists_and_eq' {α : Type u_1} {β : Type u_2} {f : α → β} {p : β → Prop} {r : α → Prop} :

(∃ (b : β), p b ∧ ∃ (a : α), r a ∧ b = f a) ↔ ∃ (a : α), r a ∧ p (f a)

theorem Disjoint.subset_iff_empty {α : Type u_1} {s t : Set α} (h : Disjoint s t) :

theorem pairwiseDisjoint_iff {β : Type u_2} {I : Type u_3} {α : I → Type u_6} (f : (i : I) → α i → β) :

(Set.univ.PairwiseDisjoint fun (i : I) => Set.range (f i)) ↔ ∀ ⦃i : I⦄ ⦃x : α i⦄ ⦃j : I⦄ ⦃y : α j⦄, f i x = f j y → i = j

theorem sigma_eq {α : Type u_1} {β : α → Sort u_6} {a a' : α} (h : a = a') {b : β a} :

noncomputable def uncurryProp {α : Type u_6} {β : α → Prop} {γ : (a : α) → β a → Sort u_7} (f : (x : α) → (y : β x) → γ x y) (x : ↑{a : α | β a}) :

γ ↑x ⋯

Auxiliary declaration for the Borel determinacy formalization.

Equations

Instances For

theorem equals_nonempty_some {α : Type u_1} {a : α} {A : Set α} {ne : A.Nonempty} (h : a = ne.some) :

a ∈ A

theorem Cardinal.choose_injection {α β : Type u} (f : α → Set β) (h : ∀ (a : α), mk α ≤ mk ↑(f a)) :

∃ (g : α → β), Function.Injective g ∧ ∀ (a : α), g a ∈ f a