Mathlib.Order.Antisymmetrization

AntisymmRel definition

(a b : α) : Prop

Full source

/-- The antisymmetrization relation `AntisymmRel r` is defined so that
`AntisymmRel r a b ↔ r a b ∧ r b a`. -/
def AntisymmRel (a b : α) : Prop :=
  r a b ∧ r b a

Antisymmetrization relation

Informal description

Given a relation $ r $ on a type $ \alpha $, the antisymmetrization relation $ \text{AntisymmRel}\, r $ is defined for elements $ a, b \in \alpha $ as $ r\, a\, b \land r\, b\, a $. This relation identifies pairs of elements that are related in both directions by $ r $.

antisymmRel_swap theorem

: AntisymmRel (swap r) = AntisymmRel r

Full source

theorem antisymmRel_swap : AntisymmRel (swap r) = AntisymmRel r :=
  funext₂ fun _ _ ↦ propext and_comm

Antisymmetrization Relation is Invariant under Swapping

Informal description

For any relation $r$ on a type $\alpha$, the antisymmetrization relation of the swapped relation $\operatorname{swap} r$ is equal to the antisymmetrization relation of $r$. That is, $\text{AntisymmRel}\, (\operatorname{swap} r) = \text{AntisymmRel}\, r$.

antisymmRel_swap_apply theorem

: AntisymmRel (swap r) a b ↔ AntisymmRel r a b

Full source

theorem antisymmRel_swap_apply : AntisymmRelAntisymmRel (swap r) a b ↔ AntisymmRel r a b :=
  and_comm

Antisymmetrization Relation is Invariant under Argument Swapping

Informal description

For any relation $r$ on a type $\alpha$ and elements $a, b \in \alpha$, the antisymmetrization relation $\text{AntisymmRel}\, (\operatorname{swap} r)\, a\, b$ holds if and only if $\text{AntisymmRel}\, r\, a\, b$ holds. In other words, swapping the arguments of $r$ does not change the antisymmetrization relation.

AntisymmRel.refl theorem

[IsRefl α r] (a : α) : AntisymmRel r a a

Full source

@[simp, refl]
theorem AntisymmRel.refl [IsRefl α r] (a : α) : AntisymmRel r a a :=
  ⟨_root_.refl _, _root_.refl _⟩

Reflexivity of the Antisymmetrization Relation

Informal description

For any reflexive relation $r$ on a type $\alpha$ and any element $a \in \alpha$, the antisymmetrization relation $\text{AntisymmRel}\, r$ satisfies $\text{AntisymmRel}\, r\, a\, a$.

AntisymmRel.rfl theorem

[IsRefl α r] {a : α} : AntisymmRel r a a

Full source

lemma AntisymmRel.rfl [IsRefl α r] {a : α} : AntisymmRel r a a := .refl ..

Reflexivity of the Antisymmetrization Relation

Informal description

For any reflexive relation $r$ on a type $\alpha$ and any element $a \in \alpha$, the antisymmetrization relation $\text{AntisymmRel}\, r$ satisfies $\text{AntisymmRel}\, r\, a\, a$.

instIsReflAntisymmRel instance

[IsRefl α r] : IsRefl α (AntisymmRel r)

Full source

instance [IsRefl α r] : IsRefl α (AntisymmRel r) where
  refl := .refl r

Reflexivity of the Antisymmetrization Relation

Informal description

For any reflexive relation $r$ on a type $\alpha$, the antisymmetrization relation $\text{AntisymmRel}\, r$ is also reflexive. That is, for every $a \in \alpha$, we have $\text{AntisymmRel}\, r\, a\, a$.

AntisymmRel.of_eq theorem

[IsRefl α r] {a b : α} (h : a = b) : AntisymmRel r a b

Full source

theorem AntisymmRel.of_eq [IsRefl α r] {a b : α} (h : a = b) : AntisymmRel r a b := h ▸ .rfl

Equality Implies Antisymmetrization Relation for Reflexive Relations

Informal description

For any reflexive relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$, if $a = b$, then the antisymmetrization relation $\text{AntisymmRel}\, r\, a\, b$ holds.

AntisymmRel.symm theorem

: AntisymmRel r a b → AntisymmRel r b a

Full source

@[symm]
theorem AntisymmRel.symm : AntisymmRel r a b → AntisymmRel r b a :=
  And.symm

Symmetry of the Antisymmetrization Relation

Informal description

For any relation $ r $ on a type $ \alpha $ and any elements $ a, b \in \alpha $, if $ \text{AntisymmRel}\, r\, a\, b $ holds (i.e., $ r\, a\, b $ and $ r\, b\, a $ both hold), then $ \text{AntisymmRel}\, r\, b\, a $ also holds.

instIsSymmAntisymmRel instance

: IsSymm α (AntisymmRel r)

Full source

instance : IsSymm α (AntisymmRel r) where
  symm _ _ := AntisymmRel.symm

Symmetry of the Antisymmetrization Relation

Informal description

The antisymmetrization relation $\text{AntisymmRel}\, r$ on a type $\alpha$ is symmetric for any relation $r$ on $\alpha$. That is, for any elements $a, b \in \alpha$, if $\text{AntisymmRel}\, r\, a\, b$ holds, then $\text{AntisymmRel}\, r\, b\, a$ also holds.

antisymmRel_comm theorem

: AntisymmRel r a b ↔ AntisymmRel r b a

Full source

theorem antisymmRel_comm : AntisymmRelAntisymmRel r a b ↔ AntisymmRel r b a :=
  And.comm

Symmetry of the Antisymmetrization Relation

Informal description

For any relation $r$ on a type $\alpha$ and any elements $a, b \in \alpha$, the antisymmetrization relation $\text{AntisymmRel}\, r\, a\, b$ holds if and only if $\text{AntisymmRel}\, r\, b\, a$ holds. In other words, $\text{AntisymmRel}\, r$ is symmetric.

AntisymmRel.trans theorem

[IsTrans α r] (hab : AntisymmRel r a b) (hbc : AntisymmRel r b c) : AntisymmRel r a c

Full source

@[trans]
theorem AntisymmRel.trans [IsTrans α r] (hab : AntisymmRel r a b) (hbc : AntisymmRel r b c) :
    AntisymmRel r a c :=
  ⟨_root_.trans hab.1 hbc.1, _root_.trans hbc.2 hab.2⟩

Transitivity of the Antisymmetrization Relation

Informal description

Let $r$ be a transitive relation on a type $\alpha$. For any elements $a, b, c \in \alpha$, if $a$ and $b$ are related in both directions by $r$ (i.e., $r\, a\, b$ and $r\, b\, a$ hold), and similarly $b$ and $c$ are related in both directions by $r$, then $a$ and $c$ are also related in both directions by $r$.

instIsTransAntisymmRel instance

[IsTrans α r] : IsTrans α (AntisymmRel r)

Full source

instance [IsTrans α r] : IsTrans α (AntisymmRel r) where
  trans _ _ _ := .trans

Transitivity of the Antisymmetrization Relation

Informal description

For any type $\alpha$ with a transitive relation $r$, the antisymmetrization relation $\text{AntisymmRel}\, r$ is also transitive.

AntisymmRel.decidableRel instance

[DecidableRel r] : DecidableRel (AntisymmRel r)

Full source

instance AntisymmRel.decidableRel [DecidableRel r] : DecidableRel (AntisymmRel r) :=
  fun _ _ ↦ instDecidableAnd

Decidability of the Antisymmetrization Relation

Informal description

For any decidable relation $ r $ on a type $ \alpha $, the antisymmetrization relation $ \text{AntisymmRel}\, r $ is also decidable. That is, for any $ a, b \in \alpha $, it is decidable whether both $ r\, a\, b $ and $ r\, b\, a $ hold.

antisymmRel_iff_eq theorem

[IsRefl α r] [IsAntisymm α r] : AntisymmRel r a b ↔ a = b

Full source

@[simp]
theorem antisymmRel_iff_eq [IsRefl α r] [IsAntisymm α r] : AntisymmRelAntisymmRel r a b ↔ a = b :=
  antisymm_iff

Antisymmetrization Relation Characterizes Equality in Reflexive and Antisymmetric Relations

Informal description

Let $\alpha$ be a type with a reflexive and antisymmetric relation $r$. Then for any elements $a, b \in \alpha$, the antisymmetrization relation $\text{AntisymmRel}\, r\, a\, b$ holds if and only if $a = b$.

AntisymmRel.le theorem

(h : AntisymmRel (· ≤ ·) a b) : a ≤ b

Full source

theorem AntisymmRel.le (h : AntisymmRel (· ≤ ·) a b) : a ≤ b := h.1

Forward implication of antisymmetrization relation

Informal description

For any elements $ a $ and $ b $ in a preorder $ \alpha $, if $ a $ and $ b $ are related in both directions (i.e., $ a \leq b $ and $ b \leq a $), then $ a \leq b $.

AntisymmRel.ge theorem

(h : AntisymmRel (· ≤ ·) a b) : b ≤ a

Full source

theorem AntisymmRel.ge (h : AntisymmRel (· ≤ ·) a b) : b ≤ a := h.2

Reverse inequality in antisymmetrization relation

Informal description

For any elements $a$ and $b$ in a preorder, if $a$ and $b$ are related in both directions (i.e., $a \leq b$ and $b \leq a$), then $b \leq a$ holds.

AntisymmRel.setoid definition

: Setoid α

Full source

/-- The antisymmetrization relation as an equivalence relation. -/
@[simps]
def AntisymmRel.setoid : Setoid α :=
  ⟨AntisymmRel r, .refl r, .symm, .trans⟩

Antisymmetrization setoid

Informal description

The setoid (equivalence relation) on a type $\alpha$ induced by the antisymmetrization relation, where two elements are equivalent if they are related in both directions by the given relation $r$. Specifically, the equivalence relation is defined by reflexivity, symmetry, and transitivity of the relation $\text{AntisymmRel}\, r$.

Antisymmetrization definition

: Type _

Full source

/-- The partial order derived from a preorder by making pairwise comparable elements equal. This is
the quotient by `fun a b => a ≤ b ∧ b ≤ a`. -/
def Antisymmetrization : Type _ :=
  Quotient <| AntisymmRel.setoid α r

Antisymmetrization of a preorder

Informal description

The partial order obtained from a preorder $\alpha$ by quotienting out the equivalence relation where two elements $a$ and $b$ are equivalent if both $a \leq b$ and $b \leq a$ hold. This construction turns any preorder into a partial order by identifying elements that are mutually comparable in both directions.

toAntisymmetrization definition

: α → Antisymmetrization α r

Full source

/-- Turn an element into its antisymmetrization. -/
def toAntisymmetrization : α → Antisymmetrization α r :=
  Quotient.mk _

Canonical map to antisymmetrization of a preorder

Informal description

The function maps an element $a$ of a preorder $\alpha$ to its equivalence class in the antisymmetrization of $\alpha$, which is the quotient of $\alpha$ by the relation identifying elements that are mutually comparable in both directions.

ofAntisymmetrization definition

: Antisymmetrization α r → α

Full source

/-- Get a representative from the antisymmetrization. -/
noncomputable def ofAntisymmetrization : Antisymmetrization α r → α :=
  Quotient.out

Representative from antisymmetrization

Informal description

The function maps an equivalence class in the antisymmetrization of a preorder $\alpha$ to a representative element of $\alpha$ from that equivalence class.

instInhabitedAntisymmetrization instance

[Inhabited α] : Inhabited (Antisymmetrization α r)

Full source

instance [Inhabited α] : Inhabited (Antisymmetrization α r) := by
  unfold Antisymmetrization; infer_instance

Inhabited Antisymmetrization of a Preorder

Informal description

For any preorder $\alpha$ with an inhabited instance, the antisymmetrization of $\alpha$ is also inhabited.

Antisymmetrization.ind theorem

{p : Antisymmetrization α r → Prop} : (∀ a, p <| toAntisymmetrization r a) → ∀ q, p q

Full source

@[elab_as_elim]
protected theorem Antisymmetrization.ind {p : Antisymmetrization α r → Prop} :
    (∀ a, p <| toAntisymmetrization r a) → ∀ q, p q :=
  Quot.ind

Induction Principle for Antisymmetrization of a Preorder

Informal description

For any predicate $p$ on the antisymmetrization of a preorder $\alpha$ with respect to a relation $r$, if $p$ holds for the image of every element $a \in \alpha$ under the canonical map $\text{toAntisymmetrization}\, r$, then $p$ holds for every element $q$ of the antisymmetrization $\text{Antisymmetrization}\, \alpha\, r$.

Antisymmetrization.induction_on theorem

{p : Antisymmetrization α r → Prop} (a : Antisymmetrization α r) (h : ∀ a, p <| toAntisymmetrization r a) : p a

Full source

@[elab_as_elim]
protected theorem Antisymmetrization.induction_on {p : Antisymmetrization α r → Prop}
    (a : Antisymmetrization α r) (h : ∀ a, p <| toAntisymmetrization r a) : p a :=
  Quotient.inductionOn' a h

Induction Principle for Antisymmetrization of a Preorder

Informal description

For any predicate $p$ on the antisymmetrization of a preorder $\alpha$ with respect to a relation $r$, if $p$ holds for the image of every element of $\alpha$ under the canonical map $\text{toAntisymmetrization}\, r$, then $p$ holds for every element of the antisymmetrization.

toAntisymmetrization_ofAntisymmetrization theorem

(a : Antisymmetrization α r) : toAntisymmetrization r (ofAntisymmetrization r a) = a

Full source

@[simp]
theorem toAntisymmetrization_ofAntisymmetrization (a : Antisymmetrization α r) :
    toAntisymmetrization r (ofAntisymmetrization r a) = a :=
  Quotient.out_eq' _

Canonical Map from Antisymmetrization is Left Inverse

Informal description

For any equivalence class $a$ in the antisymmetrization of a preorder $\alpha$ with respect to a relation $r$, the canonical map to the antisymmetrization of $\alpha$ applied to a representative of $a$ returns $a$ itself. In other words, $\text{toAntisymmetrization}\, r (\text{ofAntisymmetrization}\, r\, a) = a$.

le_iff_lt_or_antisymmRel theorem

: a ≤ b ↔ a < b ∨ AntisymmRel (· ≤ ·) a b

Full source

theorem le_iff_lt_or_antisymmRel : a ≤ b ↔ a < b ∨ AntisymmRel (· ≤ ·) a b := by
  rw [lt_iff_le_not_le, AntisymmRel]
  tauto

Characterization of Preorder Relation via Strict Order or Antisymmetry

Informal description

For any elements $a$ and $b$ in a preorder, $a \leq b$ if and only if either $a < b$ or $a$ and $b$ are related in both directions (i.e., $a \leq b$ and $b \leq a$).

le_of_le_of_antisymmRel theorem

(h₁ : a ≤ b) (h₂ : AntisymmRel (· ≤ ·) b c) : a ≤ c

Full source

theorem le_of_le_of_antisymmRel (h₁ : a ≤ b) (h₂ : AntisymmRel (· ≤ ·) b c) : a ≤ c :=
  h₁.trans h₂.le

Transitivity of Preorder Relation under Antisymmetric Condition

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $a \leq b$ and $b$ is antisymmetrically related to $c$ (i.e., $b \leq c$ and $c \leq b$), then $a \leq c$.

le_of_antisymmRel_of_le theorem

(h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : b ≤ c) : a ≤ c

Full source

theorem le_of_antisymmRel_of_le (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : b ≤ c) : a ≤ c :=
  h₁.le.trans h₂

Transitivity of Preorder Relation under Antisymmetric Condition: $a \sim b$ and $b \leq c$ implies $a \leq c$

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $a$ and $b$ are related in both directions (i.e., $a \leq b$ and $b \leq a$) and $b \leq c$, then $a \leq c$.

lt_of_lt_of_antisymmRel theorem

(h₁ : a < b) (h₂ : AntisymmRel (· ≤ ·) b c) : a < c

Full source

theorem lt_of_lt_of_antisymmRel (h₁ : a < b) (h₂ : AntisymmRel (· ≤ ·) b c) : a < c :=
  h₁.trans_le h₂.le

Strict Inequality Preservation under Antisymmetric Relation: $a < b$ and $b \sim c$ implies $a < c$

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $a < b$ and $b$ is antisymmetrically related to $c$ (i.e., $b \leq c$ and $c \leq b$), then $a < c$.

lt_of_antisymmRel_of_lt theorem

(h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : b < c) : a < c

Full source

theorem lt_of_antisymmRel_of_lt (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : b < c) : a < c :=
  h₁.le.trans_lt h₂

Strict Inequality Preservation under Antisymmetric Relation: $a \sim b$ and $b < c$ implies $a < c$

Informal description

For any elements $a$, $b$, and $c$ in a preorder, if $a$ and $b$ are related in both directions (i.e., $a \leq b$ and $b \leq a$) and $b < c$, then $a < c$.

instTransLeAntisymmRel instance

: @Trans α α α (· ≤ ·) (AntisymmRel (· ≤ ·)) (· ≤ ·)

Full source

instance : @Trans α α α (· ≤ ·) (AntisymmRel (· ≤ ·)) (· ≤ ·) where
  trans := le_of_le_of_antisymmRel

Transitivity of Preorder with Antisymmetric Relation

Informal description

For any preorder $\alpha$, the relation $\leq$ is transitive with respect to the antisymmetric relation $\text{AntisymmRel}\, (\leq)$. That is, if $a \leq b$ and $b \sim c$, then $a \leq c$, where $b \sim c$ means $b \leq c$ and $c \leq b$.

instTransAntisymmRelLe instance

: @Trans α α α (AntisymmRel (· ≤ ·)) (· ≤ ·) (· ≤ ·)

Full source

instance : @Trans α α α (AntisymmRel (· ≤ ·)) (· ≤ ·) (· ≤ ·) where
  trans := le_of_antisymmRel_of_le

Transitivity of Antisymmetric Relation with Preorder

Informal description

For any preorder $\alpha$, the relation $\text{AntisymmRel}\, (\le)$ is transitive with respect to $\le$. That is, if $a \sim b$ and $b \le c$, then $a \le c$, where $a \sim b$ means $a \le b$ and $b \le a$.

instTransLtAntisymmRelLe instance

: @Trans α α α (· < ·) (AntisymmRel (· ≤ ·)) (· < ·)

Full source

instance : @Trans α α α (· < ·) (AntisymmRel (· ≤ ·)) (· < ·) where
  trans := lt_of_lt_of_antisymmRel

Transitivity of Strict Order with Antisymmetric Relation

Informal description

For any preorder $\alpha$, the relation $<$ is transitive with respect to the antisymmetric relation $\text{AntisymmRel}\, (\le)$. That is, if $a < b$ and $b \sim c$, then $a < c$, where $b \sim c$ means $b \le c$ and $c \le b$.

instTransAntisymmRelLeLt instance

: @Trans α α α (AntisymmRel (· ≤ ·)) (· < ·) (· < ·)

Full source

instance : @Trans α α α (AntisymmRel (· ≤ ·)) (· < ·) (· < ·) where
  trans := lt_of_antisymmRel_of_lt

Transitivity of Antisymmetric Relation with Strict Order

Informal description

For any preorder $\alpha$, the relation $\text{AntisymmRel}\, (\le)$ is transitive with respect to $<$. That is, if $a \sim b$ and $b < c$, then $a < c$, where $a \sim b$ means $a \le b$ and $b \le a$.

AntisymmRel.le_congr theorem

(h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) : a ≤ c ↔ b ≤ d

Full source

theorem AntisymmRel.le_congr (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) :
    a ≤ c ↔ b ≤ d where
  mp h := (h₁.symm.trans_le h).trans_antisymmRel h₂
  mpr h := (h₁.trans_le h).trans_antisymmRel h₂.symm

Order Congruence under Antisymmetric Relation

Informal description

For any elements $a, b, c, d$ in a preorder $\alpha$, if $a$ and $b$ are related both ways by $\leq$ (i.e., $a \leq b$ and $b \leq a$), and $c$ and $d$ are related both ways by $\leq$, then $a \leq c$ if and only if $b \leq d$.

AntisymmRel.le_congr_left theorem

(h : AntisymmRel (· ≤ ·) a b) : a ≤ c ↔ b ≤ c

Full source

theorem AntisymmRel.le_congr_left (h : AntisymmRel (· ≤ ·) a b) : a ≤ c ↔ b ≤ c :=
  h.le_congr .rfl

Left Order Congruence under Antisymmetric Relation

Informal description

For any elements $a, b, c$ in a preorder $\alpha$, if $a$ and $b$ are related both ways by $\leq$ (i.e., $a \leq b$ and $b \leq a$), then $a \leq c$ if and only if $b \leq c$.

AntisymmRel.le_congr_right theorem

(h : AntisymmRel (· ≤ ·) b c) : a ≤ b ↔ a ≤ c

Full source

theorem AntisymmRel.le_congr_right (h : AntisymmRel (· ≤ ·) b c) : a ≤ b ↔ a ≤ c :=
  AntisymmRel.rfl.le_congr h

Right Order Congruence under Antisymmetric Relation

Informal description

For any elements $a, b, c$ in a preorder $\alpha$, if $b$ and $c$ are related both ways by $\leq$ (i.e., $b \leq c$ and $c \leq b$), then $a \leq b$ if and only if $a \leq c$.

AntisymmRel.lt_congr theorem

(h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) : a < c ↔ b < d

Full source

theorem AntisymmRel.lt_congr (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) :
    a < c ↔ b < d where
  mp h := (h₁.symm.trans_lt h).trans_antisymmRel h₂
  mpr h := (h₁.trans_lt h).trans_antisymmRel h₂.symm

Strict Inequality Congruence under Antisymmetrization

Informal description

For any elements $a, b, c, d$ in a preorder and given that $a$ and $b$ are related both ways by the relation $\leq$ (i.e., $a \leq b$ and $b \leq a$), and similarly $c$ and $d$ are related both ways by $\leq$, then $a < c$ if and only if $b < d$.

AntisymmRel.lt_congr_left theorem

(h : AntisymmRel (· ≤ ·) a b) : a < c ↔ b < c

Full source

theorem AntisymmRel.lt_congr_left (h : AntisymmRel (· ≤ ·) a b) : a < c ↔ b < c :=
  h.lt_congr .rfl

Left Strict Inequality Congruence under Antisymmetrization

Informal description

For any elements $a, b, c$ in a preorder, if $a$ and $b$ are related both ways by the relation $\leq$ (i.e., $a \leq b$ and $b \leq a$), then $a < c$ if and only if $b < c$.

AntisymmRel.lt_congr_right theorem

(h : AntisymmRel (· ≤ ·) b c) : a < b ↔ a < c

Full source

theorem AntisymmRel.lt_congr_right (h : AntisymmRel (· ≤ ·) b c) : a < b ↔ a < c :=
  AntisymmRel.rfl.lt_congr h

Right Congruence of Strict Inequality under Antisymmetrization

Informal description

For any elements $a, b, c$ in a preorder $(α, ≤)$, if $b$ and $c$ are related by the antisymmetrization relation (i.e., $b \leq c$ and $c \leq b$), then the strict inequality $a < b$ holds if and only if $a < c$ holds.

AntisymmRel.antisymmRel_congr theorem

 (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) : AntisymmRel (· ≤ ·) a c ↔ AntisymmRel (· ≤ ·) b d

Full source

theorem AntisymmRel.antisymmRel_congr
    (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) c d) :
    AntisymmRelAntisymmRel (· ≤ ·) a c ↔ AntisymmRel (· ≤ ·) b d :=
  rel_congr h₁ h₂

Congruence of Antisymmetrization Relation for Pairs of Elements

Informal description

For any elements $a, b, c, d$ in a preorder $(α, ≤)$, if $a$ and $b$ are related by the antisymmetrization relation (i.e., $a ≤ b$ and $b ≤ a$) and $c$ and $d$ are related by the antisymmetrization relation (i.e., $c ≤ d$ and $d ≤ c$), then the antisymmetrization relation between $a$ and $c$ is equivalent to the antisymmetrization relation between $b$ and $d$. In other words: $$ (a ≤ c ∧ c ≤ a) ↔ (b ≤ d ∧ d ≤ b) $$

AntisymmRel.antisymmRel_congr_left theorem

(h : AntisymmRel (· ≤ ·) a b) : AntisymmRel (· ≤ ·) a c ↔ AntisymmRel (· ≤ ·) b c

Full source

theorem AntisymmRel.antisymmRel_congr_left (h : AntisymmRel (· ≤ ·) a b) :
    AntisymmRelAntisymmRel (· ≤ ·) a c ↔ AntisymmRel (· ≤ ·) b c :=
  rel_congr_left h

Left Congruence of Antisymmetrization Relation

Informal description

For any elements $a, b, c$ in a preorder $(α, ≤)$, if $a$ and $b$ are related by the antisymmetrization relation (i.e., $a ≤ b$ and $b ≤ a$), then the antisymmetrization relation between $a$ and $c$ is equivalent to the antisymmetrization relation between $b$ and $c$. In other words: $$ (a ≤ c ∧ c ≤ a) ↔ (b ≤ c ∧ c ≤ b) $$

AntisymmRel.antisymmRel_congr_right theorem

(h : AntisymmRel (· ≤ ·) b c) : AntisymmRel (· ≤ ·) a b ↔ AntisymmRel (· ≤ ·) a c

Full source

theorem AntisymmRel.antisymmRel_congr_right (h : AntisymmRel (· ≤ ·) b c) :
    AntisymmRelAntisymmRel (· ≤ ·) a b ↔ AntisymmRel (· ≤ ·) a c :=
  rel_congr_right h

Right Congruence of Antisymmetrization Relation

Informal description

For any elements $a, b, c$ in a preorder $(α, ≤)$, if $b$ and $c$ are related by the antisymmetrization relation (i.e., $b ≤ c$ and $c ≤ b$), then the antisymmetrization relation between $a$ and $b$ is equivalent to the antisymmetrization relation between $a$ and $c$. In other words: $$ (a ≤ b ∧ b ≤ a) ↔ (a ≤ c ∧ c ≤ a) $$

AntisymmRel.image theorem

(h : AntisymmRel (· ≤ ·) a b) {f : α → β} (hf : Monotone f) : AntisymmRel (· ≤ ·) (f a) (f b)

Full source

theorem AntisymmRel.image (h : AntisymmRel (· ≤ ·) a b) {f : α → β} (hf : Monotone f) :
    AntisymmRel (· ≤ ·) (f a) (f b) :=
  ⟨hf h.1, hf h.2⟩

Monotone Functions Preserve Antisymmetrization Relation

Informal description

Let $\leq$ be a preorder on a type $\alpha$, and let $a, b \in \alpha$ be such that $a \leq b$ and $b \leq a$ (i.e., $a$ and $b$ are related by the antisymmetrization relation). If $f : \alpha \to \beta$ is a monotone function (with respect to $\leq$ on $\alpha$ and $\beta$), then $f(a)$ and $f(b)$ are also related by the antisymmetrization relation on $\beta$, i.e., $f(a) \leq f(b)$ and $f(b) \leq f(a)$.

instPartialOrderAntisymmetrization instance

: PartialOrder (Antisymmetrization α (· ≤ ·))

Full source

instance instPartialOrderAntisymmetrization : PartialOrder (Antisymmetrization α (· ≤ ·)) where
  le :=
    Quotient.lift₂ (· ≤ ·) fun (_ _ _ _ : α) h₁ h₂ =>
      propext ⟨fun h => h₁.2.trans <| h.trans h₂.1, fun h => h₁.1.trans <| h.trans h₂.2⟩
  lt :=
    Quotient.lift₂ (· < ·) fun (_ _ _ _ : α) h₁ h₂ =>
      propext ⟨fun h => h₁.2.trans_lt <| h.trans_le h₂.1, fun h =>
                h₁.1.trans_lt <| h.trans_le h₂.2⟩
  le_refl a := Quotient.inductionOn' a le_refl
  le_trans a b c := Quotient.inductionOn₃' a b c fun _ _ _ => le_trans
  lt_iff_le_not_le a b := Quotient.inductionOn₂' a b fun _ _ => lt_iff_le_not_le
  le_antisymm a b := Quotient.inductionOn₂' a b fun _ _ hab hba => Quotient.sound' ⟨hab, hba⟩

Partial Order Structure on Antisymmetrization of a Preorder

Informal description

For any preorder $\alpha$, the antisymmetrization $\text{Antisymmetrization}\,\alpha$ is a partial order, where elements are considered equivalent if they are related in both directions by the preorder relation $\leq$.

antisymmetrization_fibration theorem

: Relation.Fibration (· < ·) (· < ·) (toAntisymmetrization (α := α) (· ≤ ·))

Full source

theorem antisymmetrization_fibration :
    Relation.Fibration (· < ·) (· < ·) (toAntisymmetrization (α := α) (· ≤ ·)) := by
  rintro a ⟨b⟩ h
  exact ⟨b, h, rfl⟩

Fibration Property of the Antisymmetrization Map

Informal description

The canonical map $\text{toAntisymmetrization} : \alpha \to \text{Antisymmetrization}\,\alpha$ is a fibration between the strict order relations $(<)$ on $\alpha$ and $(<)$ on $\text{Antisymmetrization}\,\alpha$. That is, for any $a \in \alpha$ and any equivalence class $[b] \in \text{Antisymmetrization}\,\alpha$ such that $[b] < \text{toAntisymmetrization}(a)$, there exists $a' \in \alpha$ with $a' < a$ and $\text{toAntisymmetrization}(a') = [b]$.

acc_antisymmetrization_iff theorem

: Acc (· < ·) (toAntisymmetrization (α := α) (· ≤ ·) a) ↔ Acc (· < ·) a

Full source

theorem acc_antisymmetrization_iff : AccAcc (· < ·)
    (toAntisymmetrization (α := α) (· ≤ ·) a) ↔ Acc (· < ·) a :=
  acc_lift₂_iff

Accessibility Equivalence in Antisymmetrization and Original Preorder

Informal description

For any element $a$ in a preorder $\alpha$, the equivalence class of $a$ in the antisymmetrization of $\alpha$ is accessible with respect to the strict order relation $<$ if and only if $a$ itself is accessible with respect to $<$ in $\alpha$.

wellFounded_antisymmetrization_iff theorem

: WellFounded (@LT.lt (Antisymmetrization α (· ≤ ·)) _) ↔ WellFounded (@LT.lt α _)

Full source

theorem wellFounded_antisymmetrization_iff :
    WellFoundedWellFounded (@LT.lt (Antisymmetrization α (· ≤ ·)) _) ↔ WellFounded (@LT.lt α _) :=
  wellFounded_lift₂_iff

Well-foundedness of Antisymmetrization $\leftrightarrow$ Well-foundedness of Original Preorder

Informal description

For a preorder $\alpha$, the strict order relation $<$ on the antisymmetrization $\text{Antisymmetrization}\,\alpha$ is well-founded if and only if the strict order relation $<$ on $\alpha$ is well-founded.

wellFoundedLT_antisymmetrization_iff theorem

: WellFoundedLT (Antisymmetrization α (· ≤ ·)) ↔ WellFoundedLT α

Full source

theorem wellFoundedLT_antisymmetrization_iff :
    WellFoundedLTWellFoundedLT (Antisymmetrization α (· ≤ ·)) ↔ WellFoundedLT α := by
  simp_rw [isWellFounded_iff, wellFounded_antisymmetrization_iff]

Well-Foundedness of Antisymmetrization $\leftrightarrow$ Well-Foundedness of Original Preorder

Informal description

For any preorder $\alpha$, the antisymmetrization $\text{Antisymmetrization}\,\alpha$ is well-founded with respect to the strict order relation $<$ if and only if the original preorder $\alpha$ is well-founded with respect to $<$.

wellFoundedGT_antisymmetrization_iff theorem

: WellFoundedGT (Antisymmetrization α (· ≤ ·)) ↔ WellFoundedGT α

Full source

theorem wellFoundedGT_antisymmetrization_iff :
    WellFoundedGTWellFoundedGT (Antisymmetrization α (· ≤ ·)) ↔ WellFoundedGT α := by
  simp_rw [isWellFounded_iff]
  convert wellFounded_liftOn₂'_iff with ⟨_⟩ ⟨_⟩
  exact fun _ _ _ _ h₁ h₂ ↦ propext
    ⟨fun h ↦ (h₂.2.trans_lt h).trans_le h₁.1, fun h ↦ (h₂.1.trans_lt h).trans_le h₁.2⟩

Well-Foundedness of Antisymmetrization with Respect to Greater-Than $\leftrightarrow$ Well-Foundedness of Original Preorder

Informal description

For any preorder $\alpha$, the antisymmetrization $\text{Antisymmetrization}\,\alpha$ is well-founded with respect to the strict greater-than relation $>$ if and only if the original preorder $\alpha$ is well-founded with respect to $>$.

instWellFoundedLTAntisymmetrizationLe instance

[WellFoundedLT α] : WellFoundedLT (Antisymmetrization α (· ≤ ·))

Full source

instance [WellFoundedLT α] : WellFoundedLT (Antisymmetrization α (· ≤ ·)) :=
  wellFoundedLT_antisymmetrization_iff.mpr ‹_›

Well-Foundedness of Antisymmetrization Preserved from Preorder

Informal description

For any preorder $\alpha$ that is well-founded with respect to the strict order relation $<$, its antisymmetrization $\text{Antisymmetrization}\,\alpha$ is also well-founded with respect to $<$.

instWellFoundedGTAntisymmetrizationLe instance

[WellFoundedGT α] : WellFoundedGT (Antisymmetrization α (· ≤ ·))

Full source

instance [WellFoundedGT α] : WellFoundedGT (Antisymmetrization α (· ≤ ·)) :=
  wellFoundedGT_antisymmetrization_iff.mpr ‹_›

Well-Foundedness of Antisymmetrization with Respect to Greater-Than Preserved from Preorder

Informal description

For any preorder $\alpha$ that is well-founded with respect to the strict greater-than relation $>$, its antisymmetrization $\text{Antisymmetrization}\,\alpha$ is also well-founded with respect to $>$.

instLinearOrderAntisymmetrizationLeOfDecidableLEOfDecidableLTOfIsTotal instance

[DecidableLE α] [DecidableLT α] [IsTotal α (· ≤ ·)] : LinearOrder (Antisymmetrization α (· ≤ ·))

Full source

instance [DecidableLE α] [DecidableLT α] [IsTotal α (· ≤ ·)] :
    LinearOrder (Antisymmetrization α (· ≤ ·)) :=
  { instPartialOrderAntisymmetrization with
    le_total := fun a b => Quotient.inductionOn₂' a b <| total_of (· ≤ ·),
    toDecidableLE := fun _ _ => show Decidable (Quotient.liftOn₂' _ _ _ _) from inferInstance,
    toDecidableLT := fun _ _ => show Decidable (Quotient.liftOn₂' _ _ _ _) from inferInstance }

Linear Order Structure on Antisymmetrization of a Total Preorder

Informal description

For any preorder $\alpha$ with decidable $\leq$ and $<$ relations and a total order relation $\leq$, the antisymmetrization of $\alpha$ forms a linear order.

toAntisymmetrization_le_toAntisymmetrization_iff theorem

: toAntisymmetrization (α := α) (· ≤ ·) a ≤ toAntisymmetrization (α := α) (· ≤ ·) b ↔ a ≤ b

Full source

@[simp]
theorem toAntisymmetrization_le_toAntisymmetrization_iff :
    toAntisymmetrizationtoAntisymmetrization (α := α) (· ≤ ·) a ≤ toAntisymmetrization (α := α) (· ≤ ·) b ↔ a ≤ b :=
  Iff.rfl

Preservation of Order under Antisymmetrization

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the image of $a$ under the canonical map to the antisymmetrization of $\alpha$ is less than or equal to the image of $b$ if and only if $a \leq b$ in the original preorder. Symbolically: $$\text{toAntisymmetrization}(a) \leq \text{toAntisymmetrization}(b) \leftrightarrow a \leq b$$

toAntisymmetrization_lt_toAntisymmetrization_iff theorem

: toAntisymmetrization (α := α) (· ≤ ·) a < toAntisymmetrization (α := α) (· ≤ ·) b ↔ a < b

Full source

@[simp]
theorem toAntisymmetrization_lt_toAntisymmetrization_iff :
    toAntisymmetrizationtoAntisymmetrization (α := α) (· ≤ ·) a < toAntisymmetrization (α := α) (· ≤ ·) b ↔ a < b :=
  Iff.rfl

Preservation of Strict Order under Antisymmetrization

Informal description

For any elements $a$ and $b$ in a preorder $\alpha$, the image of $a$ under the canonical map to the antisymmetrization of $\alpha$ is strictly less than the image of $b$ if and only if $a$ is strictly less than $b$ in the original preorder. In other words, the canonical map preserves the strict order relation. Symbolically, this can be written as: $$\text{toAntisymmetrization}\,a < \text{toAntisymmetrization}\,b \leftrightarrow a < b$$

ofAntisymmetrization_le_ofAntisymmetrization_iff theorem

 {a b : Antisymmetrization α (· ≤ ·)} : ofAntisymmetrization (· ≤ ·) a ≤ ofAntisymmetrization (· ≤ ·) b ↔ a ≤ b

Full source

@[simp]
theorem ofAntisymmetrization_le_ofAntisymmetrization_iff {a b : Antisymmetrization α (· ≤ ·)} :
    ofAntisymmetrizationofAntisymmetrization (· ≤ ·) a ≤ ofAntisymmetrization (· ≤ ·) b ↔ a ≤ b :=
  (Quotient.outRelEmbedding _).map_rel_iff

Order Correspondence in Antisymmetrization

Informal description

For any elements $a$ and $b$ in the antisymmetrization of a preorder $\alpha$, the representative of $a$ is less than or equal to the representative of $b$ in $\alpha$ if and only if $a \leq b$ in the antisymmetrization. Symbolically: $$\text{ofAntisymmetrization}\,a \leq \text{ofAntisymmetrization}\,b \leftrightarrow a \leq b$$

ofAntisymmetrization_lt_ofAntisymmetrization_iff theorem

 {a b : Antisymmetrization α (· ≤ ·)} : ofAntisymmetrization (· ≤ ·) a < ofAntisymmetrization (· ≤ ·) b ↔ a < b

Full source

@[simp]
theorem ofAntisymmetrization_lt_ofAntisymmetrization_iff {a b : Antisymmetrization α (· ≤ ·)} :
    ofAntisymmetrizationofAntisymmetrization (· ≤ ·) a < ofAntisymmetrization (· ≤ ·) b ↔ a < b :=
  (Quotient.outRelEmbedding _).map_rel_iff

Strict Order Correspondence in Antisymmetrization

Informal description

For any elements $a$ and $b$ in the antisymmetrization of a preorder $\alpha$, the representative of $a$ is strictly less than the representative of $b$ in $\alpha$ if and only if $a$ is strictly less than $b$ in the antisymmetrization. Symbolically, this can be written as: $$\text{ofAntisymmetrization}\,a < \text{ofAntisymmetrization}\,b \leftrightarrow a < b$$

toAntisymmetrization_mono theorem

: Monotone (toAntisymmetrization (α := α) (· ≤ ·))

Full source

@[mono]
theorem toAntisymmetrization_mono : Monotone (toAntisymmetrization (α := α) (· ≤ ·)) :=
  fun _ _ => id

Monotonicity of the Antisymmetrization Map

Informal description

The canonical map from a preorder $\alpha$ to its antisymmetrization $\text{Antisymmetrization}\,\alpha$ is monotone. That is, for any elements $a, b \in \alpha$ with $a \leq b$, their images under the antisymmetrization map satisfy $[a] \leq [b]$, where $[a]$ and $[b]$ denote the equivalence classes of $a$ and $b$ in the antisymmetrization.

OrderHom.antisymmetrization definition

(f : α →o β) : Antisymmetrization α (· ≤ ·) →o Antisymmetrization β (· ≤ ·)

Full source

/-- Turns an order homomorphism from `α` to `β` into one from `Antisymmetrization α` to
`Antisymmetrization β`. `Antisymmetrization` is actually a functor. See `Preorder_to_PartialOrder`.
-/
protected def OrderHom.antisymmetrization (f : α →o β) :
    AntisymmetrizationAntisymmetrization α (· ≤ ·) →o Antisymmetrization β (· ≤ ·) :=
  ⟨Quotient.map' f <| liftFun_antisymmRel f, fun a b => Quotient.inductionOn₂' a b <| f.mono⟩

Antisymmetrization of an order homomorphism

Informal description

Given an order homomorphism $ f : \alpha \to_o \beta $ between preorders, the function maps the antisymmetrization of $ \alpha $ to the antisymmetrization of $ \beta $ by applying $ f $ to representatives of equivalence classes. This function is itself an order homomorphism, meaning it preserves the order relation.

OrderHom.coe_antisymmetrization theorem

(f : α →o β) : ⇑f.antisymmetrization = Quotient.map' f (liftFun_antisymmRel f)

Full source

@[simp]
theorem OrderHom.coe_antisymmetrization (f : α →o β) :
    ⇑f.antisymmetrization = Quotient.map' f (liftFun_antisymmRel f) :=
  rfl

Commutativity of Antisymmetrization with Order Homomorphism

Informal description

For any order homomorphism $f \colon \alpha \to_o \beta$ between preorders, the underlying function of the antisymmetrization of $f$ is equal to the quotient map induced by $f$ on the antisymmetrization of $\alpha$ and $\beta$. That is, the following diagram commutes: \[ \begin{CD} \alpha @>{f}>> \beta \\ @V{\text{toAntisymmetrization}}VV @VV{\text{toAntisymmetrization}}V \\ \text{Antisymmetrization}\,\alpha @>{f.\text{antisymmetrization}}>> \text{Antisymmetrization}\,\beta \end{CD} \] where $\text{toAntisymmetrization}$ is the canonical quotient map.

OrderHom.antisymmetrization_apply theorem

 (f : α →o β) (a : Antisymmetrization α (· ≤ ·)) : f.antisymmetrization a = Quotient.map' f (liftFun_antisymmRel f) a

Full source

theorem OrderHom.antisymmetrization_apply (f : α →o β) (a : Antisymmetrization α (· ≤ ·)) :
    f.antisymmetrization a = Quotient.map' f (liftFun_antisymmRel f) a :=
  rfl

Antisymmetrization of an Order Homomorphism Preserves Equivalence Classes

Informal description

Let $\alpha$ and $\beta$ be preorders, and let $f : \alpha \to \beta$ be an order homomorphism. For any element $[a]$ in the antisymmetrization of $\alpha$ (i.e., the quotient of $\alpha$ by the equivalence relation where $a \sim b$ if $a \leq b$ and $b \leq a$), the image of $[a]$ under the antisymmetrization of $f$ is equal to the equivalence class of $f(a)$ in the antisymmetrization of $\beta$. In other words, if we denote the quotient map by $\pi_\alpha : \alpha \to \text{Antisymmetrization}\,\alpha$ and similarly for $\beta$, then: \[ f_{\text{antisymm}}([a]) = [f(a)] \] where $f_{\text{antisymm}} : \text{Antisymmetrization}\,\alpha \to \text{Antisymmetrization}\,\beta$ is the induced order homomorphism.

OrderHom.antisymmetrization_apply_mk theorem

(f : α →o β) (a : α) : f.antisymmetrization (toAntisymmetrization _ a) = toAntisymmetrization _ (f a)

Full source

@[simp]
theorem OrderHom.antisymmetrization_apply_mk (f : α →o β) (a : α) :
    f.antisymmetrization (toAntisymmetrization _ a) = toAntisymmetrization _ (f a) :=
  @Quotient.map_mk _ _ (_root_.id _) (_root_.id _) f (liftFun_antisymmRel f) _

Antisymmetrization of an Order Homomorphism Preserves Equivalence Classes

Informal description

For any order homomorphism $f \colon \alpha \to_o \beta$ between preorders and any element $a \in \alpha$, the antisymmetrization of $f$ applied to the equivalence class of $a$ in $\text{Antisymmetrization}\,\alpha\,(\leq)$ equals the equivalence class of $f(a)$ in $\text{Antisymmetrization}\,\beta\,(\leq)$. In other words, the following diagram commutes: \[ \begin{CD} \alpha @>{f}>> \beta \\ @V{\text{toAntisymmetrization}}VV @VV{\text{toAntisymmetrization}}V \\ \text{Antisymmetrization}\,\alpha\,(\leq) @>{f.\text{antisymmetrization}}>> \text{Antisymmetrization}\,\beta\,(\leq) \end{CD} \]

OrderEmbedding.ofAntisymmetrization definition

: Antisymmetrization α (· ≤ ·) ↪o α

Full source

/-- `ofAntisymmetrization` as an order embedding. -/
@[simps]
noncomputable def OrderEmbedding.ofAntisymmetrization : AntisymmetrizationAntisymmetrization α (· ≤ ·) ↪o α :=
  { Quotient.outRelEmbedding _ with toFun := _root_.ofAntisymmetrization _ }

Order embedding from antisymmetrization to original preorder

Informal description

The order embedding that maps an equivalence class in the antisymmetrization of a preorder $\alpha$ (with respect to the relation $\leq$) to a representative element in $\alpha$. This embedding preserves and reflects the order relation, meaning for any two equivalence classes $[a], [b] \in \text{Antisymmetrization}\,\alpha\,(\leq)$, we have $[a] \leq [b]$ if and only if their representatives satisfy $a \leq b$ in $\alpha$.

OrderIso.dualAntisymmetrization definition

: (Antisymmetrization α (· ≤ ·))ᵒᵈ ≃o Antisymmetrization αᵒᵈ (· ≤ ·)

Full source

/-- `Antisymmetrization` and `orderDual` commute. -/
def OrderIso.dualAntisymmetrization :
    (Antisymmetrization α (· ≤ ·))ᵒᵈ(Antisymmetrization α (· ≤ ·))ᵒᵈ ≃o Antisymmetrization αᵒᵈ (· ≤ ·) where
  toFun := (Quotient.map' id) fun _ _ => And.symm
  invFun := (Quotient.map' id) fun _ _ => And.symm
  left_inv a := Quotient.inductionOn' a fun a => by simp_rw [Quotient.map'_mk'', id]
  right_inv a := Quotient.inductionOn' a fun a => by simp_rw [Quotient.map'_mk'', id]
  map_rel_iff' := @fun a b => Quotient.inductionOn₂' a b fun _ _ => Iff.rfl

Order isomorphism between dual antisymmetrizations

Informal description

The order isomorphism between the order dual of the antisymmetrization of a preorder $\alpha$ and the antisymmetrization of the order dual of $\alpha$. Specifically, it establishes an equivalence between $(\text{Antisymmetrization}\,\alpha\,(\leq))^\text{op}$ and $\text{Antisymmetrization}\,(\alpha^\text{op})\,(\leq)$, where $\alpha^\text{op}$ denotes the order dual of $\alpha$. The isomorphism maps elements by preserving their underlying values while flipping the order relation.

OrderIso.dualAntisymmetrization_apply theorem

(a : α) : OrderIso.dualAntisymmetrization _ (toDual <| toAntisymmetrization _ a) = toAntisymmetrization _ (toDual a)

Full source

@[simp]
theorem OrderIso.dualAntisymmetrization_apply (a : α) :
    OrderIso.dualAntisymmetrization _ (toDual <| toAntisymmetrization _ a) =
      toAntisymmetrization _ (toDual a) :=
  rfl

Application of Order Isomorphism between Dual Antisymmetrizations

Informal description

For any element $a$ in a preorder $\alpha$, the order isomorphism between the dual antisymmetrizations maps the equivalence class of $a$ in the dual of the antisymmetrization of $\alpha$ to the equivalence class of the dual of $a$ in the antisymmetrization of the dual of $\alpha$. More precisely, let $\text{Antisymmetrization}\,\alpha\,(\leq)$ denote the antisymmetrization of $\alpha$ with respect to the relation $\leq$, and let $\alpha^\text{op}$ denote the order dual of $\alpha$. Then, the isomorphism satisfies: \[ \text{OrderIso.dualAntisymmetrization}\,(\text{toDual}\,(\text{toAntisymmetrization}\,a)) = \text{toAntisymmetrization}\,(\text{toDual}\,a) \] where $\text{toDual}$ is the canonical map to the order dual and $\text{toAntisymmetrization}$ is the canonical map to the antisymmetrization.

OrderIso.dualAntisymmetrization_symm_apply theorem

 (a : α) :
  (OrderIso.dualAntisymmetrization _).symm (toAntisymmetrization _ <| toDual a) = toDual (toAntisymmetrization _ a)

Full source

@[simp]
theorem OrderIso.dualAntisymmetrization_symm_apply (a : α) :
    (OrderIso.dualAntisymmetrization _).symm (toAntisymmetrization _ <| toDual a) =
      toDual (toAntisymmetrization _ a) :=
  rfl

Inverse Image of Dual Antisymmetrization Map

Informal description

For any element $a$ in a preorder $\alpha$, the inverse of the order isomorphism `OrderIso.dualAntisymmetrization` maps the equivalence class of the dual element $\text{toDual}(a)$ in the antisymmetrization of $\alpha^\text{op}$ to the dual of the equivalence class of $a$ in the antisymmetrization of $\alpha$. In symbols, for $a \in \alpha$: $$(\text{OrderIso.dualAntisymmetrization})^{-1}(\text{toAntisymmetrization}(\leq)(\text{toDual}(a))) = \text{toDual}(\text{toAntisymmetrization}(\leq)(a))$$

Antisymmetrization.prodEquiv definition

: Antisymmetrization (α × β) (· ≤ ·) ≃o Antisymmetrization α (· ≤ ·) × Antisymmetrization β (· ≤ ·)

Full source

/-- The antisymmetrization of a product preorder is order isomorphic
to the product of antisymmetrizations. -/
def prodEquiv : AntisymmetrizationAntisymmetrization (α × β) (· ≤ ·) ≃o
    Antisymmetrization α (· ≤ ·) × Antisymmetrization β (· ≤ ·) where
  toFun := Quotient.lift (fun ab ↦ (⟦ab.1⟧, ⟦ab.2⟧)) fun ab₁ ab₂ h ↦
    Prod.ext (Quotient.sound ⟨h.1.1, h.2.1⟩) (Quotient.sound ⟨h.1.2, h.2.2⟩)
  invFun := Function.uncurry <| Quotient.lift₂ (fun a b ↦ ⟦(a, b)⟧)
    fun a₁ b₁ a₂ b₂ h₁ h₂ ↦ Quotient.sound ⟨⟨h₁.1, h₂.1⟩, h₁.2, h₂.2⟩
  left_inv := by rintro ⟨_⟩; rfl
  right_inv := by rintro ⟨⟨_⟩, ⟨_⟩⟩; rfl
  map_rel_iff' := by rintro ⟨_⟩ ⟨_⟩; rfl

Order isomorphism between antisymmetrization of a product preorder and product of antisymmetrizations

Informal description

The antisymmetrization of the product preorder $\alpha \times \beta$ is order isomorphic to the product of the antisymmetrizations of $\alpha$ and $\beta$. Specifically, the equivalence class of a pair $(a, b)$ in the antisymmetrization of $\alpha \times \beta$ corresponds to the pair of equivalence classes $(\llbracket a \rrbracket, \llbracket b \rrbracket)$ in the product of the antisymmetrizations of $\alpha$ and $\beta$.

Antisymmetrization.prodEquiv_apply_mk theorem

{ab} : prodEquiv α β ⟦ab⟧ = (⟦ab.1⟧, ⟦ab.2⟧)

Full source

@[simp] lemma prodEquiv_apply_mk {ab} : prodEquiv α β ⟦ab⟧ = (⟦ab.1⟧, ⟦ab.2⟧) := rfl

Image of Product Antisymmetrization under Order Isomorphism is Componentwise Antisymmetrization

Informal description

For any pair $(a, b)$ in the product preorder $\alpha \times \beta$, the image of its equivalence class under the order isomorphism $\text{prodEquiv}$ is the pair of equivalence classes $(\llbracket a \rrbracket, \llbracket b \rrbracket)$ in the product of the antisymmetrizations of $\alpha$ and $\beta$.

Antisymmetrization.prodEquiv_symm_apply_mk theorem

{a b} : (prodEquiv α β).symm (⟦a⟧, ⟦b⟧) = ⟦(a, b)⟧

Full source

@[simp] lemma prodEquiv_symm_apply_mk {a b} : (prodEquiv α β).symm (⟦a⟧, ⟦b⟧) = ⟦(a, b)⟧ := rfl

Inverse of Product Antisymmetrization Isomorphism Applied to Equivalence Classes

Informal description

For any elements $a \in \alpha$ and $b \in \beta$, the inverse of the order isomorphism $\text{prodEquiv}$ maps the pair of equivalence classes $(\llbracket a \rrbracket, \llbracket b \rrbracket)$ to the equivalence class of the pair $\llbracket (a, b) \rrbracket$ in the antisymmetrization of $\alpha \times \beta$.

Prod.wellFoundedLT instance

[WellFoundedLT α] [WellFoundedLT β] : WellFoundedLT (α × β)

Full source

instance Prod.wellFoundedLT [WellFoundedLT α] [WellFoundedLT β] : WellFoundedLT (α × β) :=
  wellFoundedLT_antisymmetrization_iff.mp <|
    (Antisymmetrization.prodEquiv α β).strictMono.wellFoundedLT

Well-Foundedness of Product Preorder

Informal description

For any preorders $\alpha$ and $\beta$ that are well-founded with respect to the strict order relation $<$, their product $\alpha \times \beta$ is also well-founded with respect to $<$.

Prod.wellFoundedGT instance

[WellFoundedGT α] [WellFoundedGT β] : WellFoundedGT (α × β)

Full source

instance Prod.wellFoundedGT [WellFoundedGT α] [WellFoundedGT β] : WellFoundedGT (α × β) :=
  wellFoundedGT_antisymmetrization_iff.mp <|
    (Antisymmetrization.prodEquiv α β).strictMono.wellFoundedGT

Well-Foundedness of Product Preorder with Respect to Greater-Than

Informal description

For any preorders $\alpha$ and $\beta$ that are well-founded with respect to the strict greater-than relation $>$, their product $\alpha \times \beta$ is also well-founded with respect to $>$.

Main declarations