Avoidance.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Countable exceptional closed unions and simultaneous configuration avoidance

abbrev OAI.Nagata.Workers.W25.IncidenceIndex line 21
Source documentation
Every positive degree and every nonnegative multiplicity vector, without bounds.
```
abbrev IncidenceIndex (r : ℕ) := {d : ℕ // 0 < d} × (Fin r → ℕ)
```
instance OAI.Nagata.Workers.W25.incidenceIndex_countable line 23
def OAI.Nagata.Workers.W25.exceptionalUnion line 27
Source documentation
Union of exactly the members of A which are proper subsets of the ambient type.
```
def exceptionalUnion {ι X : Type*} (A : ι → Set X) : Set X :=
…
```
theorem OAI.Nagata.Workers.W25.properFamily_countable line 31
Source documentation
The family occurring in the union is countable when its index type is countable.
```
theorem properFamily_countable {ι X : Type*} [Countable ι] (A : ι → Set X) :
    {S : Set X | ∃ i, A i ≠ Set.univ ∧ S = A i}.Countable := by
…
```
theorem OAI.Nagata.Workers.W25.member_eq_univ_of_avoids line 38
Source documentation
Avoiding this one union makes every supported incidence condition universal.
```
theorem member_eq_univ_of_avoids {ι X : Type*} (A : ι → Set X) {x : X}
    (hx : x ∉ exceptionalUnion A) {i : ι} (hi : x ∈ A i) : A i = Set.univ := by
…
```
Mentions: OAI.Nagata.Workers.W25.exceptionalUnion
theorem OAI.Nagata.Workers.W25.avoids_iff_supported_universal line 44
Source documentation
An explicit simultaneous quantifier: the same avoiding tuple works for all indices.
```
theorem avoids_iff_supported_universal {ι X : Type*} (A : ι → Set X) (x : X) :
    x ∉ exceptionalUnion A ↔ ∀ i, x ∈ A i → A i = Set.univ := by
…
```
Mentions: OAI.Nagata.Workers.W25.exceptionalUnion

theorem OAI.Nagata.Workers.W25.simultaneous_exclusion line 53

Source documentation

Conditional reduction, with the needed exclusion of bad universal loci explicit.

theorem simultaneous_exclusion {ι X : Type*} (A : ι → Set X) (bad : ι → Prop)
    (hproper : ∀ i, bad i → A i ≠ Set.univ) {x : X}
    (hx : x ∉ exceptionalUnion A) : ∀ i, bad i → x ∉ A i := by
…

Mentions: OAI.Nagata.Workers.W25.exceptionalUnion

theorem OAI.Nagata.Workers.W25.exists_exceptional_sequence line 61
Source documentation
Enumerate the proper loci as a natural-number sequence, padding with the empty set. This also covers the case where there are no proper members.
```
theorem exists_exceptional_sequence {ι X : Type*} [Countable ι] (A : ι → Set X) :
    ∃ E : ℕ → Set X,
      (∀ n, E n = ∅ ∨ ∃ i, A i ≠ Set.univ ∧ E n = A i) ∧
      (∀ x, (∃ n, x ∈ E n) ↔ x ∈ exceptionalUnion A) := by
…
```
Mentions: OAI.Nagata.Workers.W25.exceptionalUnion

theorem OAI.Nagata.Workers.W25.exists_nonzero_equation_of_proper_closed line 101

Source documentation

A proper relative closed locus has a nonzero multihomogeneous equation vanishing at every point of that locus.

theorem exists_nonzero_equation_of_proper_closed {r : ℕ}
    (S : Set (OrderedDistinctPoints r)) (hclosed : IsConfigurationZariskiClosed S)
    (hproper : S ≠ Set.univ) :
    ∃ F : MultihomogeneousEquation r, F.polynomial ≠ 0 ∧
      ∀ P ∈ S, equationVanishes F P.val := by
…

theorem OAI.Nagata.Workers.W25.exists_configuration_avoiding_closed_family line 129

Source documentation

Every countable family of proper relative Zariski closed subsets of the space of ordered distinct complex projective plane points has a common avoiding point.

theorem exists_configuration_avoiding_closed_family {r : ℕ} {ι : Type*} [Countable ι]
    (S : ι → Set (OrderedDistinctPoints r))
    (hclosed : ∀ i, IsConfigurationZariskiClosed (S i))
    (hproper : ∀ i, S i ≠ Set.univ) :
    ∃ P : OrderedDistinctPoints r, ∀ i, P ∉ S i := by
…

theorem OAI.Nagata.Workers.W25.exists_outside_exceptionalUnion line 150
Source documentation
The specific exceptional union of proper members of a closed incidence family has nonempty complement; it is one union for all indices simultaneously.
```
theorem exists_outside_exceptionalUnion {r : ℕ} {ι : Type*} [Countable ι]
    (A : ι → Set (OrderedDistinctPoints r))
    (hclosed : ∀ i, IsConfigurationZariskiClosed (A i)) :
    ∃ P : OrderedDistinctPoints r, P ∉ exceptionalUnion A := by
…
```
Mentions: OAI.Nagata.Workers.W25.exceptionalUnion

theorem OAI.Nagata.Workers.W25.exists_closed_exceptional_sequence line 163

Source documentation

Natural-number exceptional sequence matching the full target's quantifier shape. Its complement is nonempty and exactly the complement of the proper-locus union.

theorem exists_closed_exceptional_sequence {r : ℕ} {ι : Type*} [Countable ι]
    (A : ι → Set (OrderedDistinctPoints r))
    (hclosed : ∀ i, IsConfigurationZariskiClosed (A i)) :
    ∃ E : ℕ → Set (OrderedDistinctPoints r),
      (∀ n, IsConfigurationZariskiClosed (E n) ∧ E n ≠ Set.univ) ∧
      (∃ P, ∀ n, P ∉ E n) ∧
      (∀ P, (∀ n, P ∉ E n) ↔ P ∉ exceptionalUnion A) := by
…

Mentions: OAI.Nagata.Workers.W25.exceptionalUnion