ruc-ai4math/mathlib_handler_benchmark_410 huggingface dataset:
<VAR>α : Type u<VAR>i j : ℕ<VAR>hj : 0 < j<VAR>xs : List α<VAR>hi : i < xs.length<GOAL>(List.dropSlice i j xs).length < xs.length
<VAR>α : Type u<VAR>SizeOf α<VAR>i j : ℕ<VAR>hj : 0 < j<VAR>xs : List α<VAR>hi : i < xs.length<GOAL>sizeOf (List.dropSlice i j xs) < sizeOf xs
<VAR>α : Type u<VAR>β : Type v<VAR>p : α → Prop<VAR>f : (a : α) → p a → β<VAR>s t : List α<VAR>hs : ∀ (a : α), a ∈ s → p a<VAR>ht : ∀ (a : α), a ∈ t → p a<VAR>hf : ∀ (a a' : α) (ha : p a) (ha' : p a'), f a ha = f a' ha' → a = a'<VAR>h : s.Disjoint t<GOAL>(List.pmap f s hs).Disjoint (List.pmap f t ht)
<VAR>α : Type u<VAR>β : Type v<VAR>f : α → β<VAR>s t : List α<VAR>hf : Function.Injective f<VAR>h : s.Disjoint t<GOAL>(List.map f s).Disjoint (List.map f t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>BEq α<VAR>LawfulBEq α<VAR>f : α → β<VAR>a : α<VAR>as : List α<VAR>h : a ∈ as<GOAL>List.lookup a (List.map (fun x => (x, f x)) as) = some (f a)
<VAR>α : Type u<VAR>s : Set α<GOAL>Countable ↑s ↔ s.Countable
<VAR>α : Type u<VAR>s : Set α<VAR>Countable ↑s<GOAL>s.Countable
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Countable ↔ ∃ f, Function.Injective f
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Countable ↔ ∃ f, Set.InjOn f s
<VAR>α : Type u<VAR>s : Set α<GOAL>s.Countable ↔ Nonempty (Encodable ↑s)
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Countable<VAR>default : α<GOAL>s ⊆ Set.range (Set.enumerateCountable h default)
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Countable<VAR>default : α<GOAL>Set.range (Set.enumerateCountable h default) ⊆ insert default s
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Countable<VAR>default : α<VAR>h_mem : default ∈ s<GOAL>Set.range (Set.enumerateCountable h default) = s
<VAR>α : Type u<VAR>s : Set α<VAR>h : s.Countable<VAR>default : α<VAR>h_mem : default ∈ s<VAR>n : ℕ<GOAL>Set.enumerateCountable h default n ∈ s
<VAR>α : Type u<VAR>s₁ s₂ : Set α<VAR>h : s₁ ⊆ s₂<VAR>hs : s₂.Countable<GOAL>s₁.Countable
<VAR>β : Type v<VAR>ι : Sort x<VAR>Countable ι<VAR>f : ι → β<GOAL>(Set.range f).Countable
<VAR>α : Type u<VAR>Nonempty α<VAR>s : Set α<GOAL>s.Countable ↔ ∃ f, s ⊆ Set.range f
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Nonempty<GOAL>s.Countable ↔ ∃ f, Function.Surjective f
<VAR>α : Type u<VAR>Countable α<GOAL>Set.univ.Countable
<VAR>α : Type u<GOAL>Set.univ.Countable ↔ Countable α
<VAR>α : Type u<VAR>s : Set α<VAR>hc : s.Countable<VAR>hs : s.Nonempty<GOAL>∃ f, s = Set.range f
<VAR>α : Type u<VAR>a : α<GOAL>{a}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>hs : s.Countable<VAR>f : α → β<GOAL>(f '' s).Countable
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>f : α → β<VAR>hf : Set.MapsTo f s t<VAR>hf' : Set.InjOn f s<VAR>ht : t.Countable<GOAL>s.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set β<VAR>hs : s.Countable<VAR>f : α → β<VAR>hf : Set.InjOn f (f ⁻¹' s)<GOAL>(f ⁻¹' s).Countable
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set β<VAR>hs : s.Countable<VAR>f : α → β<VAR>hf : Function.Injective f<GOAL>(f ⁻¹' s).Countable
<VAR>α : Type u<VAR>CompleteLattice α<VAR>p : α → Prop<VAR>h : ∃ x, p x<GOAL>(∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤) ↔ ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ sSup S = ⊤
<VAR>α : Type u<VAR>p : Set α → Prop<VAR>h : ∃ s, p s<GOAL>(∃ s, (∀ (n : ℕ), p (s n)) ∧ ⋃ n, s n = Set.univ) ↔ ∃ S, S.Countable ∧ (∀ s ∈ S, p s) ∧ ⋃₀ S = Set.univ
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>f : α → β<VAR>hf : Set.InjOn f s<VAR>hs : (f '' s).Countable<GOAL>s.Countable
<VAR>α : Type u<VAR>ι : Sort x<VAR>t : ι → Set α<VAR>Countable ι<VAR>ht : ∀ (i : ι), (t i).Countable<GOAL>(⋃ i, t i).Countable
<VAR>α : Type u<VAR>ι : Sort x<VAR>Countable ι<VAR>t : ι → Set α<GOAL>(⋃ i, t i).Countable ↔ ∀ (i : ι), (t i).Countable
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : (a : α) → a ∈ s → Set β<VAR>hs : s.Countable<GOAL>(⋃ a, ⋃ (h : a ∈ s), t a h).Countable ↔ ∀ (a : α) (ha : a ∈ s), (t a ha).Countable
<VAR>α : Type u<VAR>s : Set (Set α)<VAR>hs : s.Countable<GOAL>(⋃₀ s).Countable ↔ ∀ a ∈ s, a.Countable
<VAR>α : Type u<VAR>s t : Set α<GOAL>(s ∪ t).Countable ↔ s.Countable ∧ t.Countable
<VAR>α : Type u<VAR>s t : Set α<VAR>hs : s.Countable<VAR>ht : t.Countable<GOAL>(s ∪ t).Countable
<VAR>α : Type u<VAR>s t : Set α<VAR>h : (s \ t).Countable<VAR>ht : t.Countable<GOAL>s.Countable
<VAR>α : Type u<VAR>s : Set α<VAR>a : α<GOAL>(insert a s).Countable ↔ s.Countable
<VAR>α : Type u<VAR>s : Set α<VAR>a : α<VAR>h : s.Countable<GOAL>(insert a s).Countable
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Finite<GOAL>s.Countable
<VAR>α : Type u<VAR>Subsingleton α<VAR>s : Set α<GOAL>s.Countable
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Subsingleton<GOAL>s.Countable
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>{x | IsTop x}.Countable
<VAR>α : Type u_1<VAR>PartialOrder α<GOAL>{x | IsBot x}.Countable
<VAR>α : Type u<VAR>s : Set α<VAR>hs : s.Countable<GOAL>{t | t.Finite ∧ t ⊆ s}.Countable
<VAR>α : Type u<VAR>π : α → Type u_1<VAR>Finite α<VAR>s : (a : α) → Set (π a)<VAR>hs : ∀ (a : α), (s a).Countable<GOAL>(Set.univ.pi s).Countable
<VAR>α : Type u<VAR>π : α → Type u_1<VAR>Finite α<VAR>s : (a : α) → Set (π a)<VAR>hs : ∀ (a : α), (s a).Countable<GOAL>{f | ∀ (a : α), f a ∈ s a}.Countable
<VAR>α : Type u<VAR>β : Type v<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Countable<VAR>ht : t.Countable<GOAL>(s ×ˢ t).Countable
<VAR>α : Type u<VAR>β : Type v<VAR>γ : Type w<VAR>s : Set α<VAR>t : Set β<VAR>hs : s.Countable<VAR>ht : t.Countable<VAR>f : α → β → γ<GOAL>(Set.image2 f s t).Countable
<VAR>α : Type u<VAR>β : Type v<VAR>f : β → Set α<VAR>hf : Pairwise (Disjoint on f)<VAR>s : Set α<VAR>h'f : ∀ (t : β), f t ⊆ s<VAR>hs : s.Countable<GOAL>{t | (f t).Nonempty}.Countable
<VAR>α : Type u<VAR>s : Finset α<GOAL>(↑s).Countable
<VAR>α : Type u_1<VAR>κ : Sort u_6<VAR>r : α → α → Prop<VAR>f : κ → Set α<VAR>h : Directed (fun x x_1 => x ⊆ x_1) f<GOAL>(⋃ n, f n).Pairwise r ↔ ∀ (n : κ), (f n).Pairwise r
<VAR>α : Type u_1<VAR>r : α → α → Prop<VAR>s : Set (Set α)<VAR>h : DirectedOn (fun x x_1 => x ⊆ x_1) s<GOAL>(⋃₀ s).Pairwise r ↔ ∀ a ∈ s, a.Pairwise r
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>PartialOrder α<VAR>OrderBot α<VAR>f : ι → α<VAR>g : ι' → Set ι<VAR>h : Directed (fun x x_1 => x ⊆ x_1) g<GOAL>(⋃ n, g n).PairwiseDisjoint f ↔ ∀ ⦃n : ι'⦄, (g n).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>PartialOrder α<VAR>OrderBot α<VAR>f : ι → α<VAR>s : Set (Set ι)<VAR>h : DirectedOn (fun x x_1 => x ⊆ x_1) s<GOAL>(⋃₀ s).PairwiseDisjoint f ↔ ∀ ⦃a : Set ι⦄, a ∈ s → a.PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>CompleteLattice α<VAR>s : Set ι'<VAR>g : ι' → Set ι<VAR>f : ι → α<VAR>hs : s.PairwiseDisjoint fun i' => ⨆ i ∈ g i', f i<VAR>hg : ∀ i ∈ s, (g i).PairwiseDisjoint f<GOAL>(⋃ i ∈ s, g i).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>CompleteLattice α<VAR>s : Set ι<VAR>t : Set ι'<VAR>f : ι × ι' → α<VAR>hs : s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')<VAR>ht : t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')<GOAL>(s ×ˢ t).PairwiseDisjoint f
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>ι' : Type u_5<VAR>Order.Frame α<VAR>s : Set ι<VAR>t : Set ι'<VAR>f : ι × ι' → α<GOAL>(s ×ˢ t).PairwiseDisjoint f ↔ (s.PairwiseDisjoint fun i => ⨆ i' ∈ t, f (i, i')) ∧ t.PairwiseDisjoint fun i' => ⨆ i ∈ s, f (i, i')
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>s t : Set ι<VAR>f : ι → Set α<VAR>h : (s ∪ t).PairwiseDisjoint f<GOAL>(⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i = ⋃ i ∈ s \ t, f i
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : ι → Set α<VAR>s t : Set ι<VAR>h₀ : (s ∪ t).PairwiseDisjoint f<VAR>h₁ : ∀ i ∈ s, (f i).Nonempty<VAR>h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i<GOAL>s ⊆ t
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : ι → Set α<VAR>s t : Set ι<VAR>h₀ : Pairwise (Disjoint on f)<VAR>h₁ : ∀ i ∈ s, (f i).Nonempty<VAR>h : ⋃ i ∈ s, f i ⊆ ⋃ i ∈ t, f i<GOAL>s ⊆ t
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : ι → Set α<VAR>h₀ : Pairwise (Disjoint on f)<VAR>h₁ : ∀ (i : ι), (f i).Nonempty<GOAL>Function.Injective fun s => ⋃ i ∈ s, f i
<VAR>α : Type u_1<VAR>ι : Type u_4<VAR>f : ι → Set α<VAR>s : Set ι<VAR>y : α<VAR>h_disjoint : s.PairwiseDisjoint f<VAR>hy : y ∈ ⋃ i ∈ s, f i<GOAL>∃! i, i ∈ s ∧ y ∈ f i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t : Set β<GOAL>Set.image2 SMul.smul s t = s • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t : Set β<GOAL>Set.image2 VAdd.vadd s t = s +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t : Set β<GOAL>(fun x => x.1 • x.2) '' s ×ˢ t = s • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t : Set β<GOAL>(fun x => x.1 +ᵥ x.2) '' s ×ˢ t = s +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t : Set β<VAR>b : β<GOAL>b ∈ s +ᵥ t ↔ ∃ x ∈ s, ∃ y ∈ t, x +ᵥ y = b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t : Set β<VAR>b : β<GOAL>b ∈ s • t ↔ ∃ x ∈ s, ∃ y ∈ t, x • y = b
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<GOAL>a ∈ s → b ∈ t → a +ᵥ b ∈ s +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t : Set β<VAR>a : α<VAR>b : β<GOAL>a ∈ s → b ∈ t → a • b ∈ s • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>t : Set β<GOAL>∅ +ᵥ t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>t : Set β<GOAL>∅ • t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<GOAL>s • ∅ = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<GOAL>s +ᵥ ∅ = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t : Set β<GOAL>s • t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t : Set β<GOAL>s +ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t : Set β<GOAL>(s • t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t : Set β<GOAL>(s +ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t : Set β<GOAL>s.Nonempty → t.Nonempty → (s +ᵥ t).Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t : Set β<GOAL>s.Nonempty → t.Nonempty → (s • t).Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t : Set β<GOAL>(s +ᵥ t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t : Set β<GOAL>(s • t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t : Set β<GOAL>(s +ᵥ t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t : Set β<GOAL>(s • t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>b : β<GOAL>s • {b} = (fun x => x • b) '' s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>b : β<GOAL>s +ᵥ {b} = (fun x => x +ᵥ b) '' s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>t : Set β<VAR>a : α<GOAL>{a} • t = a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>t : Set β<VAR>a : α<GOAL>{a} +ᵥ t = a +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>a : α<VAR>b : β<GOAL>{a} • {b} = {a • b}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>a : α<VAR>b : β<GOAL>{a} +ᵥ {b} = {a +ᵥ b}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ +ᵥ t₁ ⊆ s₂ +ᵥ t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ • t₁ ⊆ s₂ • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t₁ t₂ : Set β<GOAL>t₁ ⊆ t₂ → s • t₁ ⊆ s • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t₁ t₂ : Set β<GOAL>t₁ ⊆ t₂ → s +ᵥ t₁ ⊆ s +ᵥ t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s₁ s₂ : Set α<VAR>t : Set β<GOAL>s₁ ⊆ s₂ → s₁ +ᵥ t ⊆ s₂ +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s₁ s₂ : Set α<VAR>t : Set β<GOAL>s₁ ⊆ s₂ → s₁ • t ⊆ s₂ • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t u : Set β<GOAL>s +ᵥ t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a +ᵥ b ∈ u
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t u : Set β<GOAL>s • t ⊆ u ↔ ∀ a ∈ s, ∀ b ∈ t, a • b ∈ u
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s₁ s₂ : Set α<VAR>t : Set β<GOAL>s₁ ∪ s₂ +ᵥ t = s₁ +ᵥ t ∪ (s₂ +ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s₁ s₂ : Set α<VAR>t : Set β<GOAL>(s₁ ∪ s₂) • t = s₁ • t ∪ s₂ • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t₁ t₂ : Set β<GOAL>s +ᵥ (t₁ ∪ t₂) = s +ᵥ t₁ ∪ (s +ᵥ t₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t₁ t₂ : Set β<GOAL>s • (t₁ ∪ t₂) = s • t₁ ∪ s • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s₁ s₂ : Set α<VAR>t : Set β<GOAL>s₁ ∩ s₂ +ᵥ t ⊆ (s₁ +ᵥ t) ∩ (s₂ +ᵥ t)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s₁ s₂ : Set α<VAR>t : Set β<GOAL>(s₁ ∩ s₂) • t ⊆ s₁ • t ∩ s₂ • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t₁ t₂ : Set β<GOAL>s +ᵥ t₁ ∩ t₂ ⊆ (s +ᵥ t₁) ∩ (s +ᵥ t₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t₁ t₂ : Set β<GOAL>s • (t₁ ∩ t₂) ⊆ s • t₁ ∩ s • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<GOAL>(s₁ ∩ s₂) • (t₁ ∪ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<GOAL>s₁ ∩ s₂ +ᵥ (t₁ ∪ t₂) ⊆ s₁ +ᵥ t₁ ∪ (s₂ +ᵥ t₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<GOAL>s₁ ∪ s₂ +ᵥ t₁ ∩ t₂ ⊆ s₁ +ᵥ t₁ ∪ (s₂ +ᵥ t₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s₁ s₂ : Set α<VAR>t₁ t₂ : Set β<GOAL>(s₁ ∪ s₂) • (t₁ ∩ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t : Set β<GOAL>⋃ a ∈ s, a • t = s • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t : Set β<GOAL>⋃ a ∈ s, a +ᵥ t = s +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set α<VAR>t : Set β<GOAL>⋃ a ∈ t, (fun x => x • a) '' s = s • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set α<VAR>t : Set β<GOAL>⋃ a ∈ t, (fun x => x +ᵥ a) '' s = s +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>VAdd α β<VAR>s : ι → Set α<VAR>t : Set β<GOAL>(⋃ i, s i) +ᵥ t = ⋃ i, s i +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>SMul α β<VAR>s : ι → Set α<VAR>t : Set β<GOAL>(⋃ i, s i) • t = ⋃ i, s i • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>VAdd α β<VAR>s : Set α<VAR>t : ι → Set β<GOAL>s +ᵥ ⋃ i, t i = ⋃ i, s +ᵥ t i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>SMul α β<VAR>s : Set α<VAR>t : ι → Set β<GOAL>s • ⋃ i, t i = ⋃ i, s • t i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>SMul α β<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set β<GOAL>(⋃ i, ⋃ j, s i j) • t = ⋃ i, ⋃ j, s i j • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>VAdd α β<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set β<GOAL>(⋃ i, ⋃ j, s i j) +ᵥ t = ⋃ i, ⋃ j, s i j +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>SMul α β<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set β<GOAL>s • ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s • t i j
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>VAdd α β<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set β<GOAL>s +ᵥ ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s +ᵥ t i j
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>VAdd α β<VAR>s : ι → Set α<VAR>t : Set β<GOAL>(⋂ i, s i) +ᵥ t ⊆ ⋂ i, s i +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>SMul α β<VAR>s : ι → Set α<VAR>t : Set β<GOAL>(⋂ i, s i) • t ⊆ ⋂ i, s i • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>SMul α β<VAR>s : Set α<VAR>t : ι → Set β<GOAL>s • ⋂ i, t i ⊆ ⋂ i, s • t i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>VAdd α β<VAR>s : Set α<VAR>t : ι → Set β<GOAL>s +ᵥ ⋂ i, t i ⊆ ⋂ i, s +ᵥ t i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>SMul α β<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set β<GOAL>(⋂ i, ⋂ j, s i j) • t ⊆ ⋂ i, ⋂ j, s i j • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>VAdd α β<VAR>s : (i : ι) → κ i → Set α<VAR>t : Set β<GOAL>(⋂ i, ⋂ j, s i j) +ᵥ t ⊆ ⋂ i, ⋂ j, s i j +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>VAdd α β<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set β<GOAL>s +ᵥ ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s +ᵥ t i j
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>SMul α β<VAR>s : Set α<VAR>t : (i : ι) → κ i → Set β<GOAL>s • ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, s • t i j
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>t : Set β<VAR>a : α<VAR>s : Set α<GOAL>a ∈ s → a +ᵥ t ⊆ s +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>t : Set β<VAR>a : α<VAR>s : Set α<GOAL>a ∈ s → a • t ⊆ s • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>t : Set β<VAR>a : α<GOAL>(fun x => a • x) '' t = a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>t : Set β<VAR>a : α<GOAL>(fun x => a +ᵥ x) '' t = a +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>t : Set β<VAR>a : α<VAR>x : β<GOAL>x ∈ a • t ↔ ∃ y ∈ t, a • y = x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>t : Set β<VAR>a : α<VAR>x : β<GOAL>x ∈ a +ᵥ t ↔ ∃ y ∈ t, a +ᵥ y = x
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set β<VAR>a : α<VAR>b : β<GOAL>b ∈ s → a +ᵥ b ∈ a +ᵥ s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set β<VAR>a : α<VAR>b : β<GOAL>b ∈ s → a • b ∈ a • s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>a : α<GOAL>a +ᵥ ∅ = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>a : α<GOAL>a • ∅ = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set β<VAR>a : α<GOAL>a • s = ∅ ↔ s = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set β<VAR>a : α<GOAL>a +ᵥ s = ∅ ↔ s = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set β<VAR>a : α<GOAL>(a +ᵥ s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set β<VAR>a : α<GOAL>(a • s).Nonempty ↔ s.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>a : α<VAR>b : β<GOAL>a • {b} = {a • b}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>a : α<VAR>b : β<GOAL>a +ᵥ {b} = {a +ᵥ b}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s t : Set β<VAR>a : α<GOAL>s ⊆ t → a +ᵥ s ⊆ a +ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s t : Set β<VAR>a : α<GOAL>s ⊆ t → a • s ⊆ a • t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s t : Set β<VAR>a : α<GOAL>a • s ⊆ t ↔ ∀ ⦃b : β⦄, b ∈ s → a • b ∈ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s t : Set β<VAR>a : α<GOAL>a +ᵥ s ⊆ t ↔ ∀ ⦃b : β⦄, b ∈ s → a +ᵥ b ∈ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>t₁ t₂ : Set β<VAR>a : α<GOAL>a • (t₁ ∪ t₂) = a • t₁ ∪ a • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>t₁ t₂ : Set β<VAR>a : α<GOAL>a +ᵥ (t₁ ∪ t₂) = a +ᵥ t₁ ∪ (a +ᵥ t₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>t₁ t₂ : Set β<VAR>a : α<GOAL>a • (t₁ ∩ t₂) ⊆ a • t₁ ∩ a • t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>t₁ t₂ : Set β<VAR>a : α<GOAL>a +ᵥ t₁ ∩ t₂ ⊆ (a +ᵥ t₁) ∩ (a +ᵥ t₂)
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>SMul α β<VAR>a : α<VAR>s : ι → Set β<GOAL>a • ⋃ i, s i = ⋃ i, a • s i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>VAdd α β<VAR>a : α<VAR>s : ι → Set β<GOAL>a +ᵥ ⋃ i, s i = ⋃ i, a +ᵥ s i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>VAdd α β<VAR>a : α<VAR>s : (i : ι) → κ i → Set β<GOAL>a +ᵥ ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, a +ᵥ s i j
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>SMul α β<VAR>a : α<VAR>s : (i : ι) → κ i → Set β<GOAL>a • ⋃ i, ⋃ j, s i j = ⋃ i, ⋃ j, a • s i j
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>SMul α β<VAR>a : α<VAR>t : ι → Set β<GOAL>a • ⋂ i, t i ⊆ ⋂ i, a • t i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>VAdd α β<VAR>a : α<VAR>t : ι → Set β<GOAL>a +ᵥ ⋂ i, t i ⊆ ⋂ i, a +ᵥ t i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>SMul α β<VAR>a : α<VAR>t : (i : ι) → κ i → Set β<GOAL>a • ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, a • t i j
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Sort u_5<VAR>κ : ι → Sort u_6<VAR>VAdd α β<VAR>a : α<VAR>t : (i : ι) → κ i → Set β<GOAL>a +ᵥ ⋂ i, ⋂ j, t i j ⊆ ⋂ i, ⋂ j, a +ᵥ t i j
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>s : Set β<VAR>a : α<GOAL>s.Nonempty → (a • s).Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>s : Set β<VAR>a : α<GOAL>s.Nonempty → (a +ᵥ s).Nonempty
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<VAR>a : α<GOAL>a ∈ t → AddOpposite.op a +ᵥ s ⊆ s + t
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<VAR>a : α<GOAL>a ∈ t → MulOpposite.op a • s ⊆ s * t
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>MulOpposite.op '' s • t = t * s
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>AddOpposite.op '' s +ᵥ t = t + s
<VAR>α : Type u_2<VAR>Mul α<VAR>s t : Set α<GOAL>⋃ a ∈ t, MulOpposite.op a • s = s * t
<VAR>α : Type u_2<VAR>Add α<VAR>s t : Set α<GOAL>⋃ a ∈ t, AddOpposite.op a +ᵥ s = s + t
<VAR>α : Type u_2<VAR>Mul α<VAR>s t u : Set α<GOAL>s * t ⊆ u ↔ ∀ a ∈ s, a • t ⊆ u
<VAR>α : Type u_2<VAR>Add α<VAR>s t u : Set α<GOAL>s + t ⊆ u ↔ ∀ a ∈ s, a +ᵥ t ⊆ u
<VAR>α : Type u_2<VAR>Mul α<VAR>s t u : Set α<GOAL>s * t ⊆ u ↔ ∀ b ∈ t, MulOpposite.op b • s ⊆ u
<VAR>α : Type u_2<VAR>Add α<VAR>s t u : Set α<GOAL>s + t ⊆ u ↔ ∀ b ∈ t, AddOpposite.op b +ᵥ s ⊆ u
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>SMul α β<VAR>b : ι → α<VAR>c : κ → β<GOAL>Set.range b • Set.range c = Set.range fun p => b p.1 • c p.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>ι : Type u_5<VAR>κ : Type u_6<VAR>VAdd α β<VAR>b : ι → α<VAR>c : κ → β<GOAL>Set.range b +ᵥ Set.range c = Set.range fun p => b p.1 +ᵥ c p.2
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>ι : Sort u_5<VAR>a : α<VAR>f : ι → β<GOAL>a +ᵥ Set.range f = Set.range fun i => a +ᵥ f i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>ι : Sort u_5<VAR>a : α<VAR>f : ι → β<GOAL>a • Set.range f = Set.range fun i => a • f i
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VAdd α β<VAR>ι : Sort u_5<VAR>a : α<VAR>f : ι → β<GOAL>(Set.range fun i => a +ᵥ f i) = a +ᵥ Set.range f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>SMul α β<VAR>ι : Sort u_5<VAR>a : α<VAR>f : ι → β<GOAL>(Set.range fun i => a • f i) = a • Set.range f
<VAR>α : Type u_2<VAR>Add α<VAR>ι : Sort u_5<VAR>a : α<VAR>f : ι → α<GOAL>(Set.range fun i => a + f i) = a +ᵥ Set.range f
<VAR>α : Type u_2<VAR>Mul α<VAR>ι : Sort u_5<VAR>a : α<VAR>f : ι → α<GOAL>(Set.range fun i => a * f i) = a • Set.range f
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<GOAL>Set.image2 VSub.vsub s t = s -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<GOAL>(fun x => x.1 -ᵥ x.2) '' s ×ˢ t = s -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<VAR>a : α<GOAL>a ∈ s -ᵥ t ↔ ∃ x ∈ s, ∃ y ∈ t, x -ᵥ y = a
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<VAR>b c : β<VAR>hb : b ∈ s<VAR>hc : c ∈ t<GOAL>b -ᵥ c ∈ s -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>t : Set β<GOAL>∅ -ᵥ t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s : Set β<GOAL>s -ᵥ ∅ = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<GOAL>s -ᵥ t = ∅ ↔ s = ∅ ∨ t = ∅
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<GOAL>(s -ᵥ t).Nonempty ↔ s.Nonempty ∧ t.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<GOAL>s.Nonempty → t.Nonempty → (s -ᵥ t).Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<GOAL>(s -ᵥ t).Nonempty → s.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<GOAL>(s -ᵥ t).Nonempty → t.Nonempty
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s : Set β<VAR>b : β<GOAL>s -ᵥ {b} = (fun x => x -ᵥ b) '' s
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>t : Set β<VAR>b : β<GOAL>{b} -ᵥ t = (fun x => b -ᵥ x) '' t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>b c : β<GOAL>{b} -ᵥ {c} = {b -ᵥ c}
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s₁ s₂ t₁ t₂ : Set β<GOAL>s₁ ⊆ s₂ → t₁ ⊆ t₂ → s₁ -ᵥ t₁ ⊆ s₂ -ᵥ t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t₁ t₂ : Set β<GOAL>t₁ ⊆ t₂ → s -ᵥ t₁ ⊆ s -ᵥ t₂
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s₁ s₂ t : Set β<GOAL>s₁ ⊆ s₂ → s₁ -ᵥ t ⊆ s₂ -ᵥ t
<VAR>α : Type u_2<VAR>β : Type u_3<VAR>VSub α β<VAR>s t : Set β<VAR>u : Set α<GOAL>s -ᵥ t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x -ᵥ y ∈ u