theorem Minimal.minimal_iff_minimal_exists_minimal_and_le {α : Type u_1} [Preorder α] [WellFoundedLT α] {P : α → Prop} {x : α} : Minimal P x ↔ Minimal (fun (x : α) => ∃ (m' : α), Minimal P m' ∧ m' ≤ x) x ∧ P x

theorem Minimal.prop_of_minimal_exists_minimal_and_le {α : Type u_1} [PartialOrder α] [WellFoundedLT α] {P : α → Prop} {x : α} (h : Minimal (fun (x : α) => ∃ (m' : α), Minimal P m' ∧ m' ≤ x) x) : P x

theorem Minimal.minimal_iff_minimal_exists_minimal_and_le' {α : Type u_1} [PartialOrder α] [WellFoundedLT α] {P : α → Prop} {x : α} : Minimal P x ↔ Minimal (fun (x : α) => ∃ (m' : α), Minimal P m' ∧ m' ≤ x) x

theorem AddMonoidAlgebra.ideal_span_of'_image_eq_ideal_span_of'_image_minimal {k : Type u_1} {A : Type u_2} [CommSemiring k] [AddCommMonoid A] [Preorder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {s : Set A} : Ideal.span (of' k A '' s) = Ideal.span (of' k A '' {x : A | Minimal (fun (x : A) => x ∈ s) x})

theorem AddMonoidAlgebra.ideal_span_single_image_eq_ideal_span_single_image_minimal {k : Type u_1} {A : Type u_2} [CommSemiring k] [AddCommMonoid A] [Preorder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {s : Set A} : Ideal.span ((fun (x : A) => single x 1) '' s) = Ideal.span ((fun (x : A) => single x 1) '' {x : A | Minimal (fun (x : A) => x ∈ s) x})

theorem AddMonoidAlgebra.minimal_span_of'_image_iff_minimal {k : Type u_1} {A : Type u_2} [CommSemiring k] [AddCommMonoid A] [Preorder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {s : Set A} [Nontrivial k] {x : A} : Minimal (fun (x : A) => ∃ p ∈ Ideal.span (of' k A '' s), x ∈ p.support) x ∧ x ∈ s ↔ Minimal (fun (x : A) => x ∈ s) x

theorem AddMonoidAlgebra.minimal_ideal_span_single_image_iff_minimal {k : Type u_1} {A : Type u_2} [CommSemiring k] [AddCommMonoid A] [Preorder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {s : Set A} [Nontrivial k] {x : A} : Minimal (fun (x : A) => ∃ p ∈ Ideal.span ((fun (x : A) => single x 1) '' s), x ∈ p.support) x ∧ x ∈ s ↔ Minimal (fun (x : A) => x ∈ s) x

theorem AddMonoidAlgebra.minimal_ideal_span_of'_image_iff_minimal' {k : Type u_1} {A : Type u_2} [CommSemiring k] [Nontrivial k] [AddCommMonoid A] [PartialOrder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {x : A} {s : Set A} : Minimal (fun (x : A) => ∃ p ∈ Ideal.span (of' k A '' s), x ∈ p.support) x ↔ Minimal (fun (x : A) => x ∈ s) x

theorem AddMonoidAlgebra.minimal_ideal_span_single_image_iff_minimal' {k : Type u_1} {A : Type u_2} [CommSemiring k] [Nontrivial k] [AddCommMonoid A] [PartialOrder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {x : A} {s : Set A} : Minimal (fun (x : A) => ∃ p ∈ Ideal.span ((fun (x : A) => single x 1) '' s), x ∈ p.support) x ↔ Minimal (fun (x : A) => x ∈ s) x

theorem AddMonoidAlgebra.ideal_span_of'_image_eq_ideal_span_of'_image_iff {k : Type u_1} {A : Type u_2} [CommSemiring k] [Nontrivial k] [AddCommMonoid A] [PartialOrder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {s t : Set A} : Ideal.span (of' k A '' s) = Ideal.span (of' k A '' t) ↔ ∀ (x : A), Minimal (fun (x : A) => x ∈ s) x ↔ Minimal (fun (x : A) => x ∈ t) x

theorem AddMonoidAlgebra.ideal_span_single_image_eq_ideal_span_single_image_iff {k : Type u_1} {A : Type u_2} [CommSemiring k] [Nontrivial k] [AddCommMonoid A] [PartialOrder A] [WellFoundedLT A] [CanonicallyOrderedAdd A] {s t : Set A} : Ideal.span ((fun (x : A) => single x 1) '' s) = Ideal.span ((fun (x : A) => single x 1) '' t) ↔ ∀ (x : A), Minimal (fun (x : A) => x ∈ s) x ↔ Minimal (fun (x : A) => x ∈ t) x

theorem MvPolynomial.ideal_span_monomial_image_eq_ideal_span_monomial_image_minimal {σ : Type u_2} {R : Type u_1} [CommSemiring R] {s : Set (σ →₀ ℕ)} : Ideal.span ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' s) = Ideal.span ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' {x : σ →₀ ℕ | Minimal (fun (x : σ →₀ ℕ) => x ∈ s) x})

theorem MvPolynomial.minimal_ideal_span_monomial_image_iff_minimal {σ : Type u_2} {R : Type u_1} [CommSemiring R] {x : σ →₀ ℕ} {s : Set (σ →₀ ℕ)} [Nontrivial R] : Minimal (fun (x : σ →₀ ℕ) => ∃ p ∈ Ideal.span ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' s), x ∈ p.support) x ↔ Minimal (fun (x : σ →₀ ℕ) => x ∈ s) x

theorem MvPolynomial.ideal_span_monomial_image_eq_ideal_span_monomial_image_iff {σ : Type u_2} {R : Type u_1} [CommSemiring R] {s t : Set (σ →₀ ℕ)} [Nontrivial R] : Ideal.span ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' s) = Ideal.span ((fun (x : σ →₀ ℕ) => (monomial x) 1) '' t) ↔ ∀ (x : σ →₀ ℕ), Minimal (fun (x : σ →₀ ℕ) => x ∈ s) x ↔ Minimal (fun (x : σ →₀ ℕ) => x ∈ t) x

theorem MonomialOrder.span_leadingTerm_le_span_monomial {R : Type u_1} {σ : Type u_2} [CommSemiring R] {m : MonomialOrder σ} {B : Set (MvPolynomial σ R)} : Ideal.span (m.leadingTerm '' B) ≤ Ideal.span ((fun (p : MvPolynomial σ R) => (MvPolynomial.monomial (m.degree p)) 1) '' (B \ {0}))