Base approximations #

In this file, we define base approximations.

Main declarations #

ConNF.BaseApprox: A base approximation consists of a partial permutation of atoms and a partial permutation of near-litters.

source

structure ConNF.BaseApprox [ConNF.Params] :

Type u

exceptions : Rel ConNF.Atom ConNF.Atom
litters : Rel ConNF.Litter ConNF.Litter
exceptions_permutative : self.exceptions.Permutative
litters_permutative' : self.litters.Permutative
exceptions_small : ∀ (L : ConNF.Litter), ConNF.Small (Lᴬ ∩ self.exceptions.dom)

Instances For

source

instance ConNF.BaseApprox.instSuperLRelLitter [ConNF.Params] :

ConNF.SuperL ConNF.BaseApprox (Rel ConNF.Litter ConNF.Litter)

Equations

ConNF.BaseApprox.instSuperLRelLitter = { superL := ConNF.BaseApprox.litters }

source

@[simp]

theorem ConNF.BaseApprox.mk_litters [ConNF.Params] (exceptions : Rel ConNF.Atom ConNF.Atom) (litters : Rel ConNF.Litter ConNF.Litter) (exceptions_permutative : exceptions.Permutative) (litters_permutative' : litters.Permutative) (exceptions_small : ∀ (L : ConNF.Litter), ConNF.Small (Lᴬ ∩ exceptions.dom)) :

{ exceptions := exceptions, litters := litters, exceptions_permutative := exceptions_permutative, litters_permutative' := litters_permutative', exceptions_small := exceptions_small }ᴸ = litters

source

theorem ConNF.BaseApprox.ext [ConNF.Params] {ψ χ : ConNF.BaseApprox} (h₁ : ψ.exceptions = χ.exceptions) (h₂ : ψᴸ = χᴸ) :

ψ = χ

source

theorem ConNF.BaseApprox.litters_permutative [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψᴸ.Permutative

source

instance ConNF.BaseApprox.instInv [ConNF.Params] :

Inv ConNF.BaseApprox

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem ConNF.BaseApprox.inv_exceptions [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψ⁻¹.exceptions = ψ.exceptions.inv

source

@[simp]

theorem ConNF.BaseApprox.inv_litters [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψ⁻¹ᴸ = ψᴸ.inv

source

@[simp]

theorem ConNF.BaseApprox.inv_inv [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψ⁻¹⁻¹ = ψ

source

def ConNF.BaseApprox.sublitterAtoms [ConNF.Params] (ψ : ConNF.BaseApprox) (L : ConNF.Litter) :

Set ConNF.Atom

Equations

ψ.sublitterAtoms L = Lᴬ \ ψ.exceptions.dom

Instances For

source

theorem ConNF.BaseApprox.sublitterAtoms_near [ConNF.Params] (ψ : ConNF.BaseApprox) (L : ConNF.Litter) :

ψ.sublitterAtoms L ~ Lᴬ

source

def ConNF.BaseApprox.sublitter [ConNF.Params] (ψ : ConNF.BaseApprox) (L : ConNF.Litter) :

ConNF.NearLitter

Equations

ψ.sublitter L = { litter := L, atoms := ψ.sublitterAtoms L, atoms_near_litter' := ⋯ }

Instances For

source

theorem ConNF.BaseApprox.sublitter_atoms [ConNF.Params] {ψ : ConNF.BaseApprox} {L : ConNF.Litter} :

(ψ.sublitter L)ᴬ = Lᴬ \ ψ.exceptions.dom

source

theorem ConNF.BaseApprox.sublitter_subset [ConNF.Params] {ψ : ConNF.BaseApprox} {L : ConNF.Litter} :

(ψ.sublitter L)ᴬ ⊆ Lᴬ

source

theorem ConNF.BaseApprox.sublitter_atoms_disjoint [ConNF.Params] {ψ : ConNF.BaseApprox} {L : ConNF.Litter} :

Disjoint (ψ.sublitter L)ᴬ ψ.exceptions.dom

source

@[simp]

theorem ConNF.BaseApprox.inv_sublitter [ConNF.Params] (ψ : ConNF.BaseApprox) (L : ConNF.Litter) :

ψ⁻¹.sublitter L = ψ.sublitter L

source

def ConNF.BaseApprox.nearLitterEquiv [ConNF.Params] (N : ConNF.NearLitter) :

ConNF.κ ≃ ↑Nᴬ

Equations

ConNF.BaseApprox.nearLitterEquiv N = ⋯.some

Instances For

source

theorem ConNF.BaseApprox.nearLitterEquiv_injective [ConNF.Params] {N : ConNF.NearLitter} {i₁ i₂ : ConNF.κ} (h : ↑((ConNF.BaseApprox.nearLitterEquiv N) i₁) = ↑((ConNF.BaseApprox.nearLitterEquiv N) i₂)) :

i₁ = i₂

source

theorem ConNF.BaseApprox.nearLitterEquiv_congr [ConNF.Params] {N₁ N₂ : ConNF.NearLitter} {i₁ i₂ : ConNF.κ} (hN : N₁ = N₂) (hi : i₁ = i₂) :

↑((ConNF.BaseApprox.nearLitterEquiv N₁) i₁) = ↑((ConNF.BaseApprox.nearLitterEquiv N₂) i₂)

source

theorem ConNF.BaseApprox.nearLitterEquiv_mem [ConNF.Params] (N : ConNF.NearLitter) (i : ConNF.κ) :

↑((ConNF.BaseApprox.nearLitterEquiv N) i) ∈ Nᴬ

source

@[simp]

theorem ConNF.BaseApprox.nearLitterEquiv_litter [ConNF.Params] (ψ : ConNF.BaseApprox) (L : ConNF.Litter) (i : ConNF.κ) :

(↑((ConNF.BaseApprox.nearLitterEquiv (ψ.sublitter L)) i))ᴸ = L

source

theorem ConNF.BaseApprox.nearLitterEquiv_not_mem_dom [ConNF.Params] (ψ : ConNF.BaseApprox) (L : ConNF.Litter) (i : ConNF.κ) :

↑((ConNF.BaseApprox.nearLitterEquiv (ψ.sublitter L)) i) ∉ ψ.exceptions.dom

source

inductive ConNF.BaseApprox.typical [ConNF.Params] (ψ : ConNF.BaseApprox) :

Rel ConNF.Atom ConNF.Atom

mk: ∀ [inst : ConNF.Params] {ψ : ConNF.BaseApprox} (L₁ L₂ : ConNF.Litter), ψᴸ L₁ L₂ → ∀ (i : ConNF.κ), ψ.typical ↑((ConNF.BaseApprox.nearLitterEquiv (ψ.sublitter L₁)) i) ↑((ConNF.BaseApprox.nearLitterEquiv (ψ.sublitter L₂)) i)

Instances For

source

theorem ConNF.BaseApprox.typical_iff [ConNF.Params] {ψ : ConNF.BaseApprox} {a₁ a₂ : ConNF.Atom} :

ψ.typical a₁ a₂ ↔ ψᴸ a₁ᴸ a₂ᴸ ∧ ∃ (i : ConNF.κ), a₁ = ↑((ConNF.BaseApprox.nearLitterEquiv (ψ.sublitter a₁ᴸ)) i) ∧ a₂ = ↑((ConNF.BaseApprox.nearLitterEquiv (ψ.sublitter a₂ᴸ)) i)

source

theorem ConNF.BaseApprox.not_mem_dom_of_typical [ConNF.Params] {ψ : ConNF.BaseApprox} {a₁ a₂ : ConNF.Atom} (h : ψ.typical a₁ a₂) :

a₁ ∉ ψ.exceptions.dom

source

theorem ConNF.BaseApprox.typical_inv_of_typical [ConNF.Params] {ψ : ConNF.BaseApprox} {a₁ a₂ : ConNF.Atom} (h : ψ.typical a₁ a₂) :

ψ⁻¹.typical a₂ a₁

source

theorem ConNF.BaseApprox.typical_inv_iff_typical [ConNF.Params] {ψ : ConNF.BaseApprox} {a₁ a₂ : ConNF.Atom} :

ψ⁻¹.typical a₂ a₁ ↔ ψ.typical a₁ a₂

source

@[simp]

theorem ConNF.BaseApprox.inv_typical [ConNF.Params] {ψ : ConNF.BaseApprox} :

ψ⁻¹.typical = ψ.typical.inv

source

def ConNF.BaseApprox.atoms [ConNF.Params] (ψ : ConNF.BaseApprox) :

Rel ConNF.Atom ConNF.Atom

Equations

ψ.atoms = ψ.exceptions ⊔ ψ.typical

Instances For

source

instance ConNF.BaseApprox.instSuperARelAtom [ConNF.Params] :

ConNF.SuperA ConNF.BaseApprox (Rel ConNF.Atom ConNF.Atom)

Equations

ConNF.BaseApprox.instSuperARelAtom = { superA := ConNF.BaseApprox.atoms }

source

theorem ConNF.BaseApprox.atoms_def [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψᴬ = ψ.exceptions ⊔ ψ.typical

source

theorem ConNF.BaseApprox.exceptions_le_atoms [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψ.exceptions ≤ ψᴬ

source

theorem ConNF.BaseApprox.exceptions_dom_subset_atoms_dom [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψ.exceptions.dom ⊆ ψᴬ.dom

source

theorem ConNF.BaseApprox.mem_dom_atoms_of_litter_mem_dom [ConNF.Params] {ψ : ConNF.BaseApprox} {a : ConNF.Atom} (h : aᴸ ∈ ψᴸ.dom) :

a ∈ ψᴬ.dom

source

@[simp]

theorem ConNF.BaseApprox.inv_atoms [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψ⁻¹ᴬ = ψᴬ.inv

source

theorem ConNF.BaseApprox.typical_injective [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψ.typical.Injective

source

theorem ConNF.BaseApprox.typical_coinjective [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψ.typical.Coinjective

source

theorem ConNF.BaseApprox.typical_codomEqDom [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψ.typical.CodomEqDom

source

theorem ConNF.BaseApprox.typical_permutative [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψ.typical.Permutative

source

theorem ConNF.BaseApprox.exceptions_typical_disjoint [ConNF.Params] (ψ : ConNF.BaseApprox) :

Disjoint ψ.exceptions.dom ψ.typical.dom

source

theorem ConNF.BaseApprox.atoms_permutative [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψᴬ.Permutative

source

theorem ConNF.BaseApprox.atoms_image_eq_typical_image [ConNF.Params] (ψ : ConNF.BaseApprox) {s : Set ConNF.Atom} (hs : Disjoint ψ.exceptions.dom s) :

ψᴬ.image s = ψ.typical.image s

source

theorem ConNF.BaseApprox.typical_image_sublitter [ConNF.Params] (ψ : ConNF.BaseApprox) {L₁ L₂ : ConNF.Litter} (h : ψᴸ L₁ L₂) :

ψ.typical.image (ψ.sublitter L₁)ᴬ = (ψ.sublitter L₂)ᴬ

source

theorem ConNF.BaseApprox.image_near_of_near [ConNF.Params] (ψ : ConNF.BaseApprox) (s : Set ConNF.Atom) {L₁ L₂ : ConNF.Litter} (hL : ψᴸ L₁ L₂) (hsL : s ~ L₁ᴬ) :

ψᴬ.image s ~ L₂ᴬ

source

def ConNF.BaseApprox.nearLitters [ConNF.Params] (ψ : ConNF.BaseApprox) :

Rel ConNF.NearLitter ConNF.NearLitter

Equations

ψ.nearLitters N₁ N₂ = (ψᴸ N₁ᴸ N₂ᴸ ∧ N₁ᴬ ⊆ ψᴬ.dom ∧ ψᴬ.image N₁ᴬ = N₂ᴬ)

Instances For

source

instance ConNF.BaseApprox.instSuperNRelNearLitter [ConNF.Params] :

ConNF.SuperN ConNF.BaseApprox (Rel ConNF.NearLitter ConNF.NearLitter)

Equations

ConNF.BaseApprox.instSuperNRelNearLitter = { superN := ConNF.BaseApprox.nearLitters }

source

theorem ConNF.BaseApprox.nearLitters_def [ConNF.Params] (ψ : ConNF.BaseApprox) {N₁ N₂ : ConNF.NearLitter} :

ψᴺ N₁ N₂ ↔ ψᴸ N₁ᴸ N₂ᴸ ∧ N₁ᴬ ⊆ ψᴬ.dom ∧ ψᴬ.image N₁ᴬ = N₂ᴬ

source

theorem ConNF.BaseApprox.mem_dom_nearLitters [ConNF.Params] {ψ : ConNF.BaseApprox} {N : ConNF.NearLitter} (hL : Nᴸ ∈ ψᴸ.dom) (ha : ∀ a ∈ Nᴬ \ Nᴸᴬ, a ∈ ψᴬ.dom) :

N ∈ ψᴺ.dom

source

@[simp]

theorem ConNF.BaseApprox.inv_nearLitters [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψ⁻¹ᴺ = ψᴺ.inv

source

theorem ConNF.BaseApprox.atoms_subset_dom_of_nearLitters_left [ConNF.Params] {ψ : ConNF.BaseApprox} {N₁ N₂ : ConNF.NearLitter} (h : ψᴺ N₁ N₂) :

N₁ᴬ ⊆ ψᴬ.dom

source

theorem ConNF.BaseApprox.atoms_subset_dom_of_nearLitters_right [ConNF.Params] {ψ : ConNF.BaseApprox} {N₁ N₂ : ConNF.NearLitter} (h : ψᴺ N₁ N₂) :

N₂ᴬ ⊆ ψᴬ.dom

source

theorem ConNF.BaseApprox.nearLitters_injective [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψᴺ.Injective

source

theorem ConNF.BaseApprox.nearLitters_coinjective [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψᴺ.Coinjective

source

theorem ConNF.BaseApprox.nearLitters_codom_subset_dom [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψᴺ.codom ⊆ ψᴺ.dom

source

theorem ConNF.BaseApprox.nearLitters_permutative [ConNF.Params] (ψ : ConNF.BaseApprox) :

ψᴺ.Permutative

source

instance ConNF.BaseApprox.instLE [ConNF.Params] :

LE ConNF.BaseApprox

Equations

ConNF.BaseApprox.instLE = { le := fun (ψ χ : ConNF.BaseApprox) => ψ.exceptions = χ.exceptions ∧ ψᴸ ≤ χᴸ }

source

instance ConNF.BaseApprox.instPartialOrder [ConNF.Params] :

PartialOrder ConNF.BaseApprox

Equations

ConNF.BaseApprox.instPartialOrder = PartialOrder.mk ⋯

source

theorem ConNF.BaseApprox.litters_le_of_le [ConNF.Params] {ψ χ : ConNF.BaseApprox} (h : ψ ≤ χ) :

ψᴸ ≤ χᴸ

source

theorem ConNF.BaseApprox.sublitter_eq_of_le [ConNF.Params] {ψ χ : ConNF.BaseApprox} (h : ψ ≤ χ) (L : ConNF.Litter) :

ψ.sublitter L = χ.sublitter L

source

theorem ConNF.BaseApprox.typical_le_of_le [ConNF.Params] {ψ χ : ConNF.BaseApprox} (h : ψ ≤ χ) :

ψ.typical ≤ χ.typical

source

theorem ConNF.BaseApprox.atoms_le_of_le [ConNF.Params] {ψ χ : ConNF.BaseApprox} (h : ψ ≤ χ) :

ψᴬ ≤ χᴬ

source

theorem ConNF.BaseApprox.nearLitters_le_of_le [ConNF.Params] {ψ χ : ConNF.BaseApprox} (h : ψ ≤ χ) :

ψᴺ ≤ χᴺ

source

instance ConNF.BaseApprox.instBaseActionClass [ConNF.Params] :

ConNF.BaseActionClass ConNF.BaseApprox

This creates new definitions of ·ᴬ and ·ᴺ, but the instances are definitionally equal so no triangles are formed.

Equations

ConNF.BaseApprox.instBaseActionClass = { atoms := fun (ψ : ConNF.BaseApprox) => ψᴬ, atoms_oneOne := ⋯, nearLitters := fun (ψ : ConNF.BaseApprox) => ψᴺ, nearLitters_oneOne := ⋯ }

source

def ConNF.BaseApprox.addOrbitLitters [ConNF.Params] (f : ℤ → ConNF.Litter) :

Rel ConNF.Litter ConNF.Litter

Equations

ConNF.BaseApprox.addOrbitLitters f L₁ L₂ = ∃ (n : ℤ), L₁ = f n ∧ L₂ = f (n + 1)

Instances For

source

@[simp]

theorem ConNF.BaseApprox.addOrbitLitters_dom [ConNF.Params] (f : ℤ → ConNF.Litter) :

(ConNF.BaseApprox.addOrbitLitters f).dom = Set.range f

source

theorem ConNF.BaseApprox.addOrbitLitters_codomEqDom [ConNF.Params] (f : ℤ → ConNF.Litter) :

(ConNF.BaseApprox.addOrbitLitters f).CodomEqDom

source

theorem ConNF.BaseApprox.addOrbitLitters_oneOne [ConNF.Params] (f : ℤ → ConNF.Litter) (hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)) :

(ConNF.BaseApprox.addOrbitLitters f).OneOne

source

theorem ConNF.BaseApprox.addOrbitLitters_permutative [ConNF.Params] (f : ℤ → ConNF.Litter) (hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)) :

(ConNF.BaseApprox.addOrbitLitters f).Permutative

source

theorem ConNF.BaseApprox.disjoint_litters_dom_addOrbitLitters_dom [ConNF.Params] (ψ : ConNF.BaseApprox) (f : ℤ → ConNF.Litter) (hfψ : ∀ (n : ℤ), f n ∉ ψᴸ.dom) :

Disjoint ψᴸ.dom (ConNF.BaseApprox.addOrbitLitters f).dom

source

def ConNF.BaseApprox.addOrbit [ConNF.Params] (ψ : ConNF.BaseApprox) (f : ℤ → ConNF.Litter) (hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)) (hfψ : ∀ (n : ℤ), f n ∉ ψᴸ.dom) :

ConNF.BaseApprox

Equations

ψ.addOrbit f hf hfψ = { exceptions := ψ.exceptions, litters := ψ.litters ⊔ ConNF.BaseApprox.addOrbitLitters f, exceptions_permutative := ⋯, litters_permutative' := ⋯, exceptions_small := ⋯ }

Instances For

source

theorem ConNF.BaseApprox.addOrbit_litters [ConNF.Params] {ψ : ConNF.BaseApprox} {f : ℤ → ConNF.Litter} {hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)} {hfψ : ∀ (n : ℤ), f n ∉ ψᴸ.dom} :

(ψ.addOrbit f hf hfψ)ᴸ = ψᴸ ⊔ ConNF.BaseApprox.addOrbitLitters f

source

theorem ConNF.BaseApprox.le_addOrbit [ConNF.Params] {ψ : ConNF.BaseApprox} {f : ℤ → ConNF.Litter} {hf : ∀ (m n k : ℤ), f m = f n → f (m + k) = f (n + k)} {hfψ : ∀ (n : ℤ), f n ∉ ψᴸ.dom} :

ψ ≤ ψ.addOrbit f hf hfψ

source

theorem ConNF.BaseApprox.upperBound_exceptions_small [ConNF.Params] (c : Set ConNF.BaseApprox) (hc : IsChain (fun (x1 x2 : ConNF.BaseApprox) => x1 ≤ x2) c) (L : ConNF.Litter) :

ConNF.Small (Lᴬ ∩ (⨆ ψ ∈ c, ψ.exceptions).dom)

source

def ConNF.BaseApprox.upperBound [ConNF.Params] (c : Set ConNF.BaseApprox) (hc : IsChain (fun (x1 x2 : ConNF.BaseApprox) => x1 ≤ x2) c) :

ConNF.BaseApprox

An upper bound for a chain of base approximations.

Equations

ConNF.BaseApprox.upperBound c hc = { exceptions := ⨆ ψ ∈ c, ψ.exceptions, litters := ⨆ ψ ∈ c, ψᴸ, exceptions_permutative := ⋯, litters_permutative' := ⋯, exceptions_small := ⋯ }

Instances For

source

theorem ConNF.BaseApprox.le_upperBound [ConNF.Params] (c : Set ConNF.BaseApprox) (hc : IsChain (fun (x1 x2 : ConNF.BaseApprox) => x1 ≤ x2) c) (ψ : ConNF.BaseApprox) :

ψ ∈ c → ψ ≤ ConNF.BaseApprox.upperBound c hc

source

def ConNF.BaseApprox.Total [ConNF.Params] (ψ : ConNF.BaseApprox) :

Prop

Equations

ψ.Total = ∀ (L : ConNF.Litter), L ∈ ψᴸ.dom

Instances For

source

theorem ConNF.BaseApprox.Total.atoms [ConNF.Params] {ψ : ConNF.BaseApprox} (h : ψ.Total) (a : ConNF.Atom) :

a ∈ ψᴬ.dom

source

theorem ConNF.BaseApprox.Total.nearLitters [ConNF.Params] {ψ : ConNF.BaseApprox} (h : ψ.Total) (N : ConNF.NearLitter) :

N ∈ ψᴺ.dom

source

theorem ConNF.BaseApprox.Total.atoms_bijective [ConNF.Params] {ψ : ConNF.BaseApprox} (h : ψ.Total) :

ψᴬ.Bijective

source

theorem ConNF.BaseApprox.Total.litters_bijective [ConNF.Params] {ψ : ConNF.BaseApprox} (h : ψ.Total) :

ψᴸ.Bijective

source

theorem ConNF.BaseApprox.basePerm_apply_near_apply [ConNF.Params] (ψ : ConNF.BaseApprox) (h : ψ.Total) (s : Set ConNF.Atom) (L : ConNF.Litter) :

s ~ Lᴬ → ⇑(ψᴬ.toEquiv ⋯) '' s ~ ((ψᴸ.toEquiv ⋯) L)ᴬ

source

def ConNF.BaseApprox.basePerm [ConNF.Params] (ψ : ConNF.BaseApprox) (h : ψ.Total) :

ConNF.BasePerm

Equations

ψ.basePerm h = { atoms := ψᴬ.toEquiv ⋯, litters := ψᴸ.toEquiv ⋯, apply_near_apply := ⋯ }

Instances For

source

theorem ConNF.BaseApprox.basePerm_smul_atom_def [ConNF.Params] {ψ : ConNF.BaseApprox} {h : ψ.Total} {a : ConNF.Atom} :

ψ.basePerm h • a = ψᴬ.toFunction ⋯ a

source

theorem ConNF.BaseApprox.basePerm_smul_litter_def [ConNF.Params] {ψ : ConNF.BaseApprox} {h : ψ.Total} {L : ConNF.Litter} :

ψ.basePerm h • L = ψᴸ.toFunction ⋯ L

source

@[simp]

theorem ConNF.BaseApprox.basePerm_smul_atom_eq_iff [ConNF.Params] {ψ : ConNF.BaseApprox} {h : ψ.Total} {a₁ a₂ : ConNF.Atom} :

ψ.basePerm h • a₁ = a₂ ↔ ψᴬ a₁ a₂

source

@[simp]

theorem ConNF.BaseApprox.basePerm_inv_smul_atom_eq_iff [ConNF.Params] {ψ : ConNF.BaseApprox} {h : ψ.Total} {a₁ a₂ : ConNF.Atom} :

(ψ.basePerm h)⁻¹ • a₁ = a₂ ↔ ψᴬ a₂ a₁

source

@[simp]

theorem ConNF.BaseApprox.basePerm_smul_litter_eq_iff [ConNF.Params] {ψ : ConNF.BaseApprox} {h : ψ.Total} {L₁ L₂ : ConNF.Litter} :

ψ.basePerm h • L₁ = L₂ ↔ ψᴸ L₁ L₂

source

@[simp]

theorem ConNF.BaseApprox.basePerm_inv_smul_litter_eq_iff [ConNF.Params] {ψ : ConNF.BaseApprox} {h : ψ.Total} {L₁ L₂ : ConNF.Litter} :

(ψ.basePerm h)⁻¹ • L₁ = L₂ ↔ ψᴸ L₂ L₁

source

@[simp]

theorem ConNF.BaseApprox.basePerm_smul_nearLitter_eq_iff [ConNF.Params] {ψ : ConNF.BaseApprox} {h : ψ.Total} {N₁ N₂ : ConNF.NearLitter} :

ψ.basePerm h • N₁ = N₂ ↔ ψᴺ N₁ N₂

source

structure ConNF.BaseApprox.Approximates [ConNF.Params] (ψ : ConNF.BaseApprox) (π : ConNF.BasePerm) :

Prop

atoms : ∀ (a₁ a₂ : ConNF.Atom), ψᴬ a₁ a₂ → a₂ = π • a₁
nearLitters : ∀ (N₁ N₂ : ConNF.NearLitter), ψᴺ N₁ N₂ → N₂ = π • N₁

Instances For

source

theorem ConNF.BaseApprox.Approximates.litters [ConNF.Params] {ψ : ConNF.BaseApprox} {π : ConNF.BasePerm} (h : ψ.Approximates π) (L₁ L₂ : ConNF.Litter) :

ψᴸ L₁ L₂ → π • L₁ = L₂

source

theorem ConNF.BaseApprox.Approximates.mono [ConNF.Params] {ψ χ : ConNF.BaseApprox} {π : ConNF.BasePerm} (hχ : χ.Approximates π) (h : ψ ≤ χ) :

ψ.Approximates π

source

structure ConNF.BaseApprox.ExactlyApproximates [ConNF.Params] (ψ : ConNF.BaseApprox) (π : ConNF.BasePerm) extends ψ.Approximates π :

Prop

atoms : ∀ (a₁ a₂ : ConNF.Atom), ψᴬ a₁ a₂ → a₂ = π • a₁
nearLitters : ∀ (N₁ N₂ : ConNF.NearLitter), ψᴺ N₁ N₂ → N₂ = π • N₁
smul_litter : ∀ a ∉ ψ.exceptions.dom, (π • a)ᴸ = π • aᴸ
inv_smul_litter : ∀ a ∉ ψ.exceptions.dom, (π⁻¹ • a)ᴸ = π⁻¹ • aᴸ

Instances For

source

theorem ConNF.BaseApprox.ExactlyApproximates.mono [ConNF.Params] {ψ χ : ConNF.BaseApprox} {π : ConNF.BasePerm} (hχ : χ.ExactlyApproximates π) (h : ψ ≤ χ) :

ψ.ExactlyApproximates π

source

theorem ConNF.BaseApprox.ExactlyApproximates.smulSet_nearLitter [ConNF.Params] {ψ : ConNF.BaseApprox} {π : ConNF.BasePerm} {N₁ N₂ : ConNF.NearLitter} (hψ : ψ.ExactlyApproximates π) (hNπ : π • N₁ᴸ = N₂ᴸ) :

π • (N₁ᴸᴬ \ ψ.exceptions.dom) = N₂ᴸᴬ \ ψ.exceptions.dom

source

theorem ConNF.BaseApprox.Approximates.smulSet_eq_exceptions_image [ConNF.Params] {ψ : ConNF.BaseApprox} {π : ConNF.BasePerm} (hψ : ψ.Approximates π) (s : Set ConNF.Atom) (hs : s ⊆ ψ.exceptions.dom) :

π • s = ψ.exceptions.image s

source

theorem ConNF.BaseApprox.approximates_basePerm [ConNF.Params] {ψ : ConNF.BaseApprox} (h : ψ.Total) :

ψ.Approximates (ψ.basePerm h)

source

theorem ConNF.BaseApprox.exactlyApproximates_basePerm [ConNF.Params] {ψ : ConNF.BaseApprox} (h : ψ.Total) :

ψ.ExactlyApproximates (ψ.basePerm h)

Documentation

ConNF.FOA.BaseApprox

Base approximations #

Main declarations #