Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑Ctrl+↓to navigate, Ctrl+🖱️to focus. On Mac, use Cmdinstead of Ctrl.
/-
Copyright (c) 2022 Yaël Dillies. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Yaël Dillies

! This file was ported from Lean 3 source module order.antisymmetrization
! leanprover-community/mathlib commit 3353f661228bd27f632c600cd1a58b874d847c90
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Order.Hom.Basic
import Mathlib.Logic.Relation

/-!
# Turning a preorder into a partial order

This file allows to make a preorder into a partial order by quotienting out the elements `a`, `b`
such that `a ≤ b` and `b ≤ a`.

`Antisymmetrization` is a functor from `Preorder` to `PartialOrder`. See `Preorder_to_PartialOrder`.

## Main declarations

* `AntisymmRel`: The antisymmetrization relation. `AntisymmRel r a b` means that `a` and `b` are
  related both ways by `r`.
* `Antisymmetrization α r`: The quotient of `α` by `AntisymmRel r`. Even when `r` is just a
  preorder, `Antisymmetrization α` is a partial order.
-/

/- Porting Notes: There are many changes from `toAntisymmetrization (. ≤ .)` to
`@toAntisymmetrization α (· ≤ ·) _` -/

open Function OrderDual

variable {
α: Type ?u.2251
α
β: Type ?u.8688
β
:
Type _: Type (?u.7716+1)
Type _
} section Relation variable (
r: ααProp
r
:
α: Type ?u.8
α
α: Type ?u.20
α
Prop: Type
Prop
) /-- The antisymmetrization relation. -/ def
AntisymmRel: ααProp
AntisymmRel
(
a: α
a
b: α
b
:
α: Type ?u.20
α
) :
Prop: Type
Prop
:=
r: ααProp
r
a: α
a
b: α
b
r: ααProp
r
b: α
b
a: α
a
#align antisymm_rel
AntisymmRel: {α : Type u_1} → (ααProp) → ααProp
AntisymmRel
theorem
antisymmRel_swap: ∀ {α : Type u_1} (r : ααProp), AntisymmRel (swap r) = AntisymmRel r
antisymmRel_swap
:
AntisymmRel: {α : Type ?u.65} → (ααProp) → ααProp
AntisymmRel
(
swap: {α : Sort ?u.69} → {β : Sort ?u.68} → {φ : αβSort ?u.67} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y
swap
r: ααProp
r
) =
AntisymmRel: {α : Type ?u.95} → (ααProp) → ααProp
AntisymmRel
r: ααProp
r
:=
funext: ∀ {α : Sort ?u.112} {β : αSort ?u.111} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext
fun
_: ?m.127
_
=>
funext: ∀ {α : Sort ?u.130} {β : αSort ?u.129} {f g : (x : α) → β x}, (∀ (x : α), f x = g x) → f = g
funext
fun
_: ?m.141
_
=>
propext: ∀ {a b : Prop}, (a b) → a = b
propext
and_comm: ∀ {a b : Prop}, a b b a
and_comm
#align antisymm_rel_swap
antisymmRel_swap: ∀ {α : Type u_1} (r : ααProp), AntisymmRel (swap r) = AntisymmRel r
antisymmRel_swap
@[refl] theorem
antisymmRel_refl: ∀ {α : Type u_1} (r : ααProp) [inst : IsRefl α r] (a : α), AntisymmRel r a a
antisymmRel_refl
[
IsRefl: (α : Type ?u.182) → (ααProp) → Prop
IsRefl
α: Type ?u.170
α
r: ααProp
r
] (
a: α
a
:
α: Type ?u.170
α
) :
AntisymmRel: {α : Type ?u.189} → (ααProp) → ααProp
AntisymmRel
r: ααProp
r
a: α
a
a: α
a
:= ⟨
refl: ∀ {α : Type ?u.210} {r : ααProp} [inst : IsRefl α r] (a : α), r a a
refl
_: ?m.211
_
,
refl: ∀ {α : Type ?u.242} {r : ααProp} [inst : IsRefl α r] (a : α), r a a
refl
_: ?m.243
_
#align antisymm_rel_refl
antisymmRel_refl: ∀ {α : Type u_1} (r : ααProp) [inst : IsRefl α r] (a : α), AntisymmRel r a a
antisymmRel_refl
variable {
r: ?m.294
r
} @[symm] theorem
AntisymmRel.symm: ∀ {a b : α}, AntisymmRel r a bAntisymmRel r b a
AntisymmRel.symm
{
a: α
a
b: α
b
:
α: Type ?u.297
α
} :
AntisymmRel: {α : Type ?u.314} → (ααProp) → ααProp
AntisymmRel
r: ααProp
r
a: α
a
b: α
b
AntisymmRel: {α : Type ?u.323} → (ααProp) → ααProp
AntisymmRel
r: ααProp
r
b: α
b
a: α
a
:=
And.symm: ∀ {a b : Prop}, a bb a
And.symm
#align antisymm_rel.symm
AntisymmRel.symm: ∀ {α : Type u_1} {r : ααProp} {a b : α}, AntisymmRel r a bAntisymmRel r b a
AntisymmRel.symm
@[trans] theorem
AntisymmRel.trans: ∀ [inst : IsTrans α r] {a b c : α}, AntisymmRel r a bAntisymmRel r b cAntisymmRel r a c
AntisymmRel.trans
[
IsTrans: (α : Type ?u.372) → (ααProp) → Prop
IsTrans
α: Type ?u.360
α
r: ααProp
r
] {
a: α
a
b: α
b
c: α
c
:
α: Type ?u.360
α
} (
hab: AntisymmRel r a b
hab
:
AntisymmRel: {α : Type ?u.383} → (ααProp) → ααProp
AntisymmRel
r: ααProp
r
a: α
a
b: α
b
) (
hbc: AntisymmRel r b c
hbc
:
AntisymmRel: {α : Type ?u.393} → (ααProp) → ααProp
AntisymmRel
r: ααProp
r
b: α
b
c: α
c
) :
AntisymmRel: {α : Type ?u.403} → (ααProp) → ααProp
AntisymmRel
r: ααProp
r
a: α
a
c: α
c
:= ⟨
_root_.trans: ∀ {α : Type ?u.432} {r : ααProp} [inst : IsTrans α r] {a b c : α}, r a br b cr a c
_root_.trans
hab: AntisymmRel r a b
hab
.
1: ∀ {a b : Prop}, a ba
1
hbc: AntisymmRel r b c
hbc
.
1: ∀ {a b : Prop}, a ba
1
,
_root_.trans: ∀ {α : Type ?u.479} {r : ααProp} [inst : IsTrans α r] {a b c : α}, r a br b cr a c
_root_.trans
hbc: AntisymmRel r b c
hbc
.
2: ∀ {a b : Prop}, a bb
2
hab: AntisymmRel r a b
hab
.
2: ∀ {a b : Prop}, a bb
2
#align antisymm_rel.trans
AntisymmRel.trans: ∀ {α : Type u_1} {r : ααProp} [inst : IsTrans α r] {a b c : α}, AntisymmRel r a bAntisymmRel r b cAntisymmRel r a c
AntisymmRel.trans
instance
AntisymmRel.decidableRel: {α : Type u_1} → {r : ααProp} → [inst : DecidableRel r] → DecidableRel (AntisymmRel r)
AntisymmRel.decidableRel
[
DecidableRel: {α : Sort ?u.548} → (ααProp) → Sort (max1?u.548)
DecidableRel
r: ααProp
r
] :
DecidableRel: {α : Sort ?u.564} → (ααProp) → Sort (max1?u.564)
DecidableRel
(
AntisymmRel: {α : Type ?u.566} → (ααProp) → ααProp
AntisymmRel
r: ααProp
r
) := fun
_: ?m.594
_
_: ?m.597
_
=>
instDecidableAnd: {p q : Prop} → [dp : Decidable p] → [dq : Decidable q] → Decidable (p q)
instDecidableAnd
#align antisymm_rel.decidable_rel
AntisymmRel.decidableRel: {α : Type u_1} → {r : ααProp} → [inst : DecidableRel r] → DecidableRel (AntisymmRel r)
AntisymmRel.decidableRel
@[simp] theorem
antisymmRel_iff_eq: ∀ {α : Type u_1} {r : ααProp} [inst : IsRefl α r] [inst : IsAntisymm α r] {a b : α}, AntisymmRel r a b a = b
antisymmRel_iff_eq
[
IsRefl: (α : Type ?u.1000) → (ααProp) → Prop
IsRefl
α: Type ?u.988
α
r: ααProp
r
] [
IsAntisymm: (α : Type ?u.1005) → (ααProp) → Prop
IsAntisymm
α: Type ?u.988
α
r: ααProp
r
] {
a: α
a
b: α
b
:
α: Type ?u.988
α
} :
AntisymmRel: {α : Type ?u.1014} → (ααProp) → ααProp
AntisymmRel
r: ααProp
r
a: α
a
b: α
b
a: α
a
=
b: α
b
:=
antisymm_iff: ∀ {α : Type ?u.1029} {r : ααProp} [inst : IsRefl α r] [inst : IsAntisymm α r] {a b : α}, r a b r b a a = b
antisymm_iff
#align antisymm_rel_iff_eq
antisymmRel_iff_eq: ∀ {α : Type u_1} {r : ααProp} [inst : IsRefl α r] [inst : IsAntisymm α r] {a b : α}, AntisymmRel r a b a = b
antisymmRel_iff_eq
alias
antisymmRel_iff_eq: ∀ {α : Type u_1} {r : ααProp} [inst : IsRefl α r] [inst : IsAntisymm α r] {a b : α}, AntisymmRel r a b a = b
antisymmRel_iff_eq
AntisymmRel.eq: ∀ {α : Type u_1} {r : ααProp} [inst : IsRefl α r] [inst : IsAntisymm α r] {a b : α}, AntisymmRel r a ba = b
AntisymmRel.eq
_ #align antisymm_rel.eq
AntisymmRel.eq: ∀ {α : Type u_1} {r : ααProp} [inst : IsRefl α r] [inst : IsAntisymm α r] {a b : α}, AntisymmRel r a ba = b
AntisymmRel.eq
end Relation section IsPreorder variable (
α: ?m.1143
α
) (
r: ααProp
r
:
α: Type ?u.1157
α
α: Type ?u.1157
α
Prop: Type
Prop
) [
IsPreorder: (α : Type ?u.1152) → (ααProp) → Prop
IsPreorder
α: Type ?u.1157
α
r: ααProp
r
] /-- The antisymmetrization relation as an equivalence relation. -/ @[
simps: ∀ (α : Type u_1) (r : ααProp) [inst : IsPreorder α r] (a b : α), Setoid.r a b = AntisymmRel r a b
simps
] def
AntisymmRel.setoid: Setoid α
AntisymmRel.setoid
:
Setoid: Sort ?u.1174 → Sort (max1?u.1174)
Setoid
α: Type ?u.1157
α
:= ⟨
AntisymmRel: {α : Type ?u.1182} → (ααProp) → ααProp
AntisymmRel
r: ααProp
r
,
antisymmRel_refl: ∀ {α : Type ?u.1214} (r : ααProp) [inst : IsRefl α r] (a : α), AntisymmRel r a a
antisymmRel_refl
_: ?m.1215?m.1215Prop
_
,
AntisymmRel.symm: ∀ {α : Type ?u.1283} {r : ααProp} {a b : α}, AntisymmRel r a bAntisymmRel r b a
AntisymmRel.symm
,
AntisymmRel.trans: ∀ {α : Type ?u.1301} {r : ααProp} [inst : IsTrans α r] {a b c : α}, AntisymmRel r a bAntisymmRel r b cAntisymmRel r a c
AntisymmRel.trans
#align antisymm_rel.setoid
AntisymmRel.setoid: (α : Type u_1) → (r : ααProp) → [inst : IsPreorder α r] → Setoid α
AntisymmRel.setoid
#align antisymm_rel.setoid_r
AntisymmRel.setoid_r: ∀ (α : Type u_1) (r : ααProp) [inst : IsPreorder α r] (a b : α), Setoid.r a b = AntisymmRel r a b
AntisymmRel.setoid_r
/-- 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 u_1) → (r : ααProp) → [inst : IsPreorder α r] → Type u_1
Antisymmetrization
:
Type _: Type (?u.1539+1)
Type _
:=
Quotient: {α : Sort ?u.1541} → Setoid αSort ?u.1541
Quotient
<|
AntisymmRel.setoid: (α : Type ?u.1543) → (r : ααProp) → [inst : IsPreorder α r] → Setoid α
AntisymmRel.setoid
α: Type ?u.1522
α
r: ααProp
r
#align antisymmetrization
Antisymmetrization: (α : Type u_1) → (r : ααProp) → [inst : IsPreorder α r] → Type u_1
Antisymmetrization
variable {
α: ?m.1589
α
} /-- Turn an element into its antisymmetrization. -/ def
toAntisymmetrization: {α : Type u_1} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
:
α: Type ?u.1592
α
Antisymmetrization: (α : Type ?u.1611) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.1611
Antisymmetrization
α: Type ?u.1592
α
r: ααProp
r
:=
Quotient.mk: {α : Sort ?u.1629} → (s : Setoid α) → αQuotient s
Quotient.mk
_: Setoid ?m.1630
_
#align to_antisymmetrization
toAntisymmetrization: {α : Type u_1} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
/-- Get a representative from the antisymmetrization. -/ noncomputable def
ofAntisymmetrization: {α : Type u_1} → (r : ααProp) → [inst : IsPreorder α r] → Antisymmetrization α rα
ofAntisymmetrization
:
Antisymmetrization: (α : Type ?u.1711) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.1711
Antisymmetrization
α: Type ?u.1693
α
r: ααProp
r
α: Type ?u.1693
α
:=
Quotient.out': {α : Sort ?u.1729} → {s₁ : Setoid α} → Quotient s₁α
Quotient.out'
#align of_antisymmetrization
ofAntisymmetrization: {α : Type u_1} → (r : ααProp) → [inst : IsPreorder α r] → Antisymmetrization α rα
ofAntisymmetrization
instance: {α : Type u_1} → (r : ααProp) → [inst : IsPreorder α r] → [inst_1 : Inhabited α] → Inhabited (Antisymmetrization α r)
instance
[
Inhabited: Sort ?u.1775 → Sort (max1?u.1775)
Inhabited
α: Type ?u.1758
α
] :
Inhabited: Sort ?u.1778 → Sort (max1?u.1778)
Inhabited
(
Antisymmetrization: (α : Type ?u.1779) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.1779
Antisymmetrization
α: Type ?u.1758
α
r: ααProp
r
) :=

Goals accomplished! 🐙
α: Type ?u.1758

β: Type ?u.1761

r: ααProp

inst✝¹: IsPreorder α r

inst✝: Inhabited α


α: Type ?u.1758

β: Type ?u.1761

r: ααProp

inst✝¹: IsPreorder α r

inst✝: Inhabited α


α: Type ?u.1758

β: Type ?u.1761

r: ααProp

inst✝¹: IsPreorder α r

inst✝: Inhabited α


α: Type ?u.1758

β: Type ?u.1761

r: ααProp

inst✝¹: IsPreorder α r

inst✝: Inhabited α



Goals accomplished! 🐙
@[elab_as_elim] protected theorem
Antisymmetrization.ind: ∀ {p : Antisymmetrization α rProp}, (∀ (a : α), p (toAntisymmetrization r a)) → ∀ (q : Antisymmetrization α r), p q
Antisymmetrization.ind
{p :
Antisymmetrization: (α : Type ?u.1911) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.1911
Antisymmetrization
α: Type ?u.1893
α
r: ααProp
r
Prop: Type
Prop
} : (∀
a: ?m.1932
a
, p <|
toAntisymmetrization: {α : Type ?u.1935} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
r: ααProp
r
a: ?m.1932
a
) → ∀
q: ?m.1951
q
, p
q: ?m.1951
q
:=
Quot.ind: ∀ {α : Sort ?u.1956} {r : ααProp} {β : Quot rProp}, (∀ (a : α), β (Quot.mk r a)) → ∀ (q : Quot r), β q
Quot.ind
#align antisymmetrization.ind
Antisymmetrization.ind: ∀ {α : Type u_1} (r : ααProp) [inst : IsPreorder α r] {p : Antisymmetrization α rProp}, (∀ (a : α), p (toAntisymmetrization r a)) → ∀ (q : Antisymmetrization α r), p q
Antisymmetrization.ind
@[elab_as_elim] protected theorem
Antisymmetrization.induction_on: ∀ {α : Type u_1} (r : ααProp) [inst : IsPreorder α r] {p : Antisymmetrization α rProp} (a : Antisymmetrization α r), (∀ (a : α), p (toAntisymmetrization r a)) → p a
Antisymmetrization.induction_on
{p :
Antisymmetrization: (α : Type ?u.2019) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.2019
Antisymmetrization
α: Type ?u.2001
α
r: ααProp
r
Prop: Type
Prop
} (a :
Antisymmetrization: (α : Type ?u.2038) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.2038
Antisymmetrization
α: Type ?u.2001
α
r: ααProp
r
) (
h: ∀ (a : α), p (toAntisymmetrization r a)
h
: ∀
a: ?m.2045
a
, p <|
toAntisymmetrization: {α : Type ?u.2048} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
r: ααProp
r
a: ?m.2045
a
) : p a :=
Quotient.inductionOn': ∀ {α : Sort ?u.2068} {s₁ : Setoid α} {p : Quotient s₁Prop} (q : Quotient s₁), (∀ (a : α), p (Quotient.mk'' a)) → p q
Quotient.inductionOn'
a
h: ∀ (a : α), p (toAntisymmetrization r a)
h
#align antisymmetrization.induction_on
Antisymmetrization.induction_on: ∀ {α : Type u_1} (r : ααProp) [inst : IsPreorder α r] {p : Antisymmetrization α rProp} (a : Antisymmetrization α r), (∀ (a : α), p (toAntisymmetrization r a)) → p a
Antisymmetrization.induction_on
@[simp] theorem
toAntisymmetrization_ofAntisymmetrization: ∀ {α : Type u_1} (r : ααProp) [inst : IsPreorder α r] (a : Antisymmetrization α r), toAntisymmetrization r (ofAntisymmetrization r a) = a
toAntisymmetrization_ofAntisymmetrization
(a :
Antisymmetrization: (α : Type ?u.2145) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.2145
Antisymmetrization
α: Type ?u.2128
α
r: ααProp
r
) :
toAntisymmetrization: {α : Type ?u.2164} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
r: ααProp
r
(
ofAntisymmetrization: {α : Type ?u.2173} → (r : ααProp) → [inst : IsPreorder α r] → Antisymmetrization α rα
ofAntisymmetrization
r: ααProp
r
a) = a :=
Quotient.out_eq': ∀ {α : Sort ?u.2190} {s₁ : Setoid α} (q : Quotient s₁), Quotient.mk'' (Quotient.out' q) = q
Quotient.out_eq'
_: Quotient ?m.2192
_
#align to_antisymmetrization_of_antisymmetrization
toAntisymmetrization_ofAntisymmetrization: ∀ {α : Type u_1} (r : ααProp) [inst : IsPreorder α r] (a : Antisymmetrization α r), toAntisymmetrization r (ofAntisymmetrization r a) = a
toAntisymmetrization_ofAntisymmetrization
end IsPreorder section Preorder variable [
Preorder: Type ?u.6389 → Type ?u.6389
Preorder
α: Type ?u.2251
α
] [
Preorder: Type ?u.2260 → Type ?u.2260
Preorder
β: Type ?u.2238
β
] {
a: α
a
b: α
b
:
α: Type ?u.2511
α
} theorem
AntisymmRel.image: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α}, AntisymmRel (fun x x_1 => x x_1) a b∀ {f : αβ}, Monotone fAntisymmRel (fun x x_1 => x x_1) (f a) (f b)
AntisymmRel.image
{
a: α
a
b: α
b
:
α: Type ?u.2251
α
} (
h: AntisymmRel (fun x x_1 => x x_1) a b
h
:
AntisymmRel: {α : Type ?u.2271} → (ααProp) → ααProp
AntisymmRel
(· ≤ ·): ααProp
(· ≤ ·)
a: α
a
b: α
b
) {
f: αβ
f
:
α: Type ?u.2251
α
β: Type ?u.2254
β
} (
hf: Monotone f
hf
:
Monotone: {α : Type ?u.2335} → {β : Type ?u.2334} → [inst : Preorder α] → [inst : Preorder β] → (αβ) → Prop
Monotone
f: αβ
f
) :
AntisymmRel: {α : Type ?u.2379} → (ααProp) → ααProp
AntisymmRel
(· ≤ ·): ββProp
(· ≤ ·)
(
f: αβ
f
a: α
a
) (
f: αβ
f
b: α
b
) := ⟨
hf: Monotone f
hf
h: AntisymmRel (fun x x_1 => x x_1) a b
h
.
1: ∀ {a b : Prop}, a ba
1
,
hf: Monotone f
hf
h: AntisymmRel (fun x x_1 => x x_1) a b
h
.
2: ∀ {a b : Prop}, a bb
2
#align antisymm_rel.image
AntisymmRel.image: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {a b : α}, AntisymmRel (fun x x_1 => x x_1) a b∀ {f : αβ}, Monotone fAntisymmRel (fun x x_1 => x x_1) (f a) (f b)
AntisymmRel.image
instance: {α : Type u_1} → [inst : Preorder α] → PartialOrder (Antisymmetrization α fun x x_1 => x x_1)
instance
:
PartialOrder: Type ?u.2527 → Type ?u.2527
PartialOrder
(
Antisymmetrization: (α : Type ?u.2528) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.2528
Antisymmetrization
α: Type ?u.2511
α
(· ≤ ·): ααProp
(· ≤ ·)
) where le
a: ?m.2585
a
b: ?m.2588
b
:= (
Quotient.liftOn₂': {α : Sort ?u.2592} → {β : Sort ?u.2591} → {γ : Sort ?u.2590} → {s₁ : Setoid α} → {s₂ : Setoid β} → Quotient s₁Quotient s₂(f : αβγ) → (∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), Setoid.r a₁ b₁Setoid.r a₂ b₂f a₁ a₂ = f b₁ b₂) → γ
Quotient.liftOn₂'
a: ?m.2585
a
b: ?m.2588
b
(· ≤ ·): ααProp
(· ≤ ·)
) fun (
_: α
_
_: α
_
_: α
_
_: α
_
:
α: Type ?u.2511
α
)
h₁: ?m.2626
h₁
h₂: ?m.2629
h₂
=>
propext: ∀ {a b : Prop}, (a b) → a = b
propext
fun
h: ?m.2645
h
=>
h₁: ?m.2626
h₁
.
2: ∀ {a b : Prop}, a bb
2
.
trans: ∀ {α : Type ?u.2655} [inst : Preorder α] {a b c : α}, a bb ca c
trans
<|
h: ?m.2645
h
.
trans: ∀ {α : Type ?u.2672} [inst : Preorder α] {a b c : α}, a bb ca c
trans
h₂: ?m.2629
h₂
.
1: ∀ {a b : Prop}, a ba
1
, fun
h: ?m.2694
h
=>
h₁: ?m.2626
h₁
.
1: ∀ {a b : Prop}, a ba
1
.
trans: ∀ {α : Type ?u.2702} [inst : Preorder α] {a b c : α}, a bb ca c
trans
<|
h: ?m.2694
h
.
trans: ∀ {α : Type ?u.2715} [inst : Preorder α] {a b c : α}, a bb ca c
trans
h₂: ?m.2629
h₂
.
2: ∀ {a b : Prop}, a bb
2
lt
a: ?m.2750
a
b: ?m.2753
b
:= (
Quotient.liftOn₂': {α : Sort ?u.2757} → {β : Sort ?u.2756} → {γ : Sort ?u.2755} → {s₁ : Setoid α} → {s₂ : Setoid β} → Quotient s₁Quotient s₂(f : αβγ) → (∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), Setoid.r a₁ b₁Setoid.r a₂ b₂f a₁ a₂ = f b₁ b₂) → γ
Quotient.liftOn₂'
a: ?m.2750
a
b: ?m.2753
b
(· < ·): ααProp
(· < ·)
) fun (
_: α
_
_: α
_
_: α
_
_: α
_
:
α: Type ?u.2511
α
)
h₁: ?m.2796
h₁
h₂: ?m.2799
h₂
=>
propext: ∀ {a b : Prop}, (a b) → a = b
propext
fun
h: ?m.2810
h
=>
h₁: ?m.2796
h₁
.
2: ∀ {a b : Prop}, a bb
2
.
trans_lt: ∀ {α : Type ?u.2818} [inst : Preorder α] {a b c : α}, a bb < ca < c
trans_lt
<|
h: ?m.2810
h
.
trans_le: ∀ {α : Type ?u.2835} [inst : Preorder α] {a b c : α}, a < bb ca < c
trans_le
h₂: ?m.2799
h₂
.
1: ∀ {a b : Prop}, a ba
1
, fun
h: ?m.2857
h
=>
h₁: ?m.2796
h₁
.
1: ∀ {a b : Prop}, a ba
1
.
trans_lt: ∀ {α : Type ?u.2865} [inst : Preorder α] {a b c : α}, a bb < ca < c
trans_lt
<|
h: ?m.2857
h
.
trans_le: ∀ {α : Type ?u.2878} [inst : Preorder α] {a b c : α}, a < bb ca < c
trans_le
h₂: ?m.2799
h₂
.
2: ∀ {a b : Prop}, a bb
2
⟩ le_refl
a: ?m.2910
a
:=
Quotient.inductionOn': ∀ {α : Sort ?u.2912} {s₁ : Setoid α} {p : Quotient s₁Prop} (q : Quotient s₁), (∀ (a : α), p (Quotient.mk'' a)) → p q
Quotient.inductionOn'
a: ?m.2910
a
<|
le_refl: ∀ {α : Type ?u.3162} [inst : Preorder α] (a : α), a a
le_refl
le_trans
a: ?m.2944
a
b: ?m.2947
b
c: ?m.2950
c
:=
Quotient.inductionOn₃': ∀ {α : Sort ?u.2952} {β : Sort ?u.2953} {γ : Sort ?u.2954} {s₁ : Setoid α} {s₂ : Setoid β} {s₃ : Setoid γ} {p : Quotient s₁Quotient s₂Quotient s₃Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂) (q₃ : Quotient s₃), (∀ (a₁ : α) (a₂ : β) (a₃ : γ), p (Quotient.mk'' a₁) (Quotient.mk'' a₂) (Quotient.mk'' a₃)) → p q₁ q₂ q₃
Quotient.inductionOn₃'
a: ?m.2944
a
b: ?m.2947
b
c: ?m.2950
c
fun
_: ?m.3186
_
_: ?m.3189
_
_: ?m.3192
_
=>
le_trans: ∀ {α : Type ?u.3194} [inst : Preorder α] {a b c : α}, a bb ca c
le_trans
lt_iff_le_not_le
a: ?m.3034
a
b: ?m.3037
b
:=
Quotient.inductionOn₂': ∀ {α : Sort ?u.3039} {β : Sort ?u.3040} {s₁ : Setoid α} {s₂ : Setoid β} {p : Quotient s₁Quotient s₂Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂), (∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) → p q₁ q₂
Quotient.inductionOn₂'
a: ?m.3034
a
b: ?m.3037
b
fun
_: ?m.3280
_
_: ?m.3283
_
=>
lt_iff_le_not_le: ∀ {α : Type ?u.3285} [inst : Preorder α] {a b : α}, a < b a b ¬b a
lt_iff_le_not_le
le_antisymm
a: ?m.3093
a
b: ?m.3096
b
:=
Quotient.inductionOn₂': ∀ {α : Sort ?u.3098} {β : Sort ?u.3099} {s₁ : Setoid α} {s₂ : Setoid β} {p : Quotient s₁Quotient s₂Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂), (∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) → p q₁ q₂
Quotient.inductionOn₂'
a: ?m.3093
a
b: ?m.3096
b
fun
_: ?m.3328
_
_: ?m.3331
_
hab: ?m.3334
hab
hba: ?m.3337
hba
=>
Quotient.sound': ∀ {α : Sort ?u.3339} {s₁ : Setoid α} {a b : α}, Setoid.r a bQuotient.mk'' a = Quotient.mk'' b
Quotient.sound'
hab: ?m.3334
hab
,
hba: ?m.3337
hba
theorem
antisymmetrization_fibration: Relation.Fibration (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (toAntisymmetrization fun x x_1 => x x_1)
antisymmetrization_fibration
:
Relation.Fibration: {α : Type ?u.3562} → {β : Type ?u.3561} → (ααProp) → (ββProp) → (αβ) → Prop
Relation.Fibration
(· < ·): ααProp
(· < ·)
(· < ·): (Antisymmetrization α fun x x_1 => x x_1) → (Antisymmetrization α fun x x_1 => x x_1) → Prop
(· < ·)
(@
toAntisymmetrization: {α : Type ?u.3657} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
α: Type ?u.3545
α
(· ≤ ·): ααProp
(· ≤ ·)
_) :=

Goals accomplished! 🐙
α: Type u_1

β: Type ?u.3548

inst✝¹: Preorder α

inst✝: Preorder β

a, b: α


Relation.Fibration (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (toAntisymmetrization fun x x_1 => x x_1)
α: Type u_1

β: Type ?u.3548

inst✝¹: Preorder α

inst✝: Preorder β

a✝, b✝¹, a: α

b✝: Antisymmetrization α fun x x_1 => x x_1

b: α

h: Quot.mk Setoid.r b < toAntisymmetrization (fun x x_1 => x x_1) a


mk
a', (fun x x_1 => x < x_1) a' a toAntisymmetrization (fun x x_1 => x x_1) a' = Quot.mk Setoid.r b
α: Type u_1

β: Type ?u.3548

inst✝¹: Preorder α

inst✝: Preorder β

a, b: α


Relation.Fibration (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (toAntisymmetrization fun x x_1 => x x_1)

Goals accomplished! 🐙
#align antisymmetrization_fibration
antisymmetrization_fibration: ∀ {α : Type u_1} [inst : Preorder α], Relation.Fibration (fun x x_1 => x < x_1) (fun x x_1 => x < x_1) (toAntisymmetrization fun x x_1 => x x_1)
antisymmetrization_fibration
theorem
acc_antisymmetrization_iff: Acc (fun x x_1 => x < x_1) (toAntisymmetrization (fun x x_1 => x x_1) a) Acc (fun x x_1 => x < x_1) a
acc_antisymmetrization_iff
:
Acc: {α : Sort ?u.3849} → (ααProp) → αProp
Acc
(· < ·): (Antisymmetrization α fun x x_1 => x x_1) → (Antisymmetrization α fun x x_1 => x x_1) → Prop
(· < ·)
(@
toAntisymmetrization: {α : Type ?u.3897} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
α: Type ?u.3833
α
(· ≤ ·): ααProp
(· ≤ ·)
_
a: α
a
) ↔
Acc: {α : Sort ?u.3948} → (ααProp) → αProp
Acc
(· < ·): ααProp
(· < ·)
a: α
a
:=
acc_liftOn₂'_iff: ∀ {α : Type ?u.4038} {s : Setoid α} {r : ααProp} {H : ∀ (a₁ a₂ b₁ b₂ : α), Setoid.r a₁ b₁Setoid.r a₂ b₂r a₁ a₂ = r b₁ b₂} {a : α}, Acc (fun x y => Quotient.liftOn₂' x y r H) (Quotient.mk'' a) Acc r a
acc_liftOn₂'_iff
#align acc_antisymmetrization_iff
acc_antisymmetrization_iff: ∀ {α : Type u_1} [inst : Preorder α] {a : α}, Acc (fun x x_1 => x < x_1) (toAntisymmetrization (fun x x_1 => x x_1) a) Acc (fun x x_1 => x < x_1) a
acc_antisymmetrization_iff
theorem
wellFounded_antisymmetrization_iff: WellFounded LT.lt WellFounded LT.lt
wellFounded_antisymmetrization_iff
:
WellFounded: {α : Sort ?u.4117} → (ααProp) → Prop
WellFounded
(@
LT.lt: {α : Type ?u.4119} → [self : LT α] → ααProp
LT.lt
(
Antisymmetrization: (α : Type ?u.4120) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.4120
Antisymmetrization
α: Type ?u.4101
α
(· ≤ ·): ααProp
(· ≤ ·)
) _) ↔
WellFounded: {α : Sort ?u.4204} → (ααProp) → Prop
WellFounded
(@
LT.lt: {α : Type ?u.4206} → [self : LT α] → ααProp
LT.lt
α: Type ?u.4101
α
_) :=
wellFounded_liftOn₂'_iff: ∀ {α : Type ?u.4218} {s : Setoid α} {r : ααProp} {H : ∀ (a₁ a₂ b₁ b₂ : α), Setoid.r a₁ b₁Setoid.r a₂ b₂r a₁ a₂ = r b₁ b₂}, (WellFounded fun x y => Quotient.liftOn₂' x y r H) WellFounded r
wellFounded_liftOn₂'_iff
#align well_founded_antisymmetrization_iff
wellFounded_antisymmetrization_iff: ∀ {α : Type u_1} [inst : Preorder α], WellFounded LT.lt WellFounded LT.lt
wellFounded_antisymmetrization_iff
instance: ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : WellFoundedLT α], WellFoundedLT (Antisymmetrization α fun x x_1 => x x_1)
instance
[
WellFoundedLT: (α : Type ?u.4293) → [inst : LT α] → Prop
WellFoundedLT
α: Type ?u.4277
α
] :
WellFoundedLT: (α : Type ?u.4307) → [inst : LT α] → Prop
WellFoundedLT
(
Antisymmetrization: (α : Type ?u.4308) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.4308
Antisymmetrization
α: Type ?u.4277
α
(· ≤ ·): ααProp
(· ≤ ·)
) := ⟨
wellFounded_antisymmetrization_iff: ∀ {α : Type ?u.4397} [inst : Preorder α], WellFounded LT.lt WellFounded LT.lt
wellFounded_antisymmetrization_iff
.
2: ∀ {a b : Prop}, (a b) → ba
2
IsWellFounded.wf: ∀ {α : Type ?u.4435} {r : ααProp} [self : IsWellFounded α r], WellFounded r
IsWellFounded.wf
instance: {α : Type u_1} → [inst : Preorder α] → [inst_1 : DecidableRel fun x x_1 => x x_1] → [inst_2 : DecidableRel fun x x_1 => x < x_1] → [inst_3 : IsTotal α fun x x_1 => x x_1] → LinearOrder (Antisymmetrization α fun x x_1 => x x_1)
instance
[@
DecidableRel: {α : Sort ?u.4520} → (ααProp) → Sort (max1?u.4520)
DecidableRel
α: Type ?u.4504
α
(· ≤ ·): ααProp
(· ≤ ·)
] [@
DecidableRel: {α : Sort ?u.4550} → (ααProp) → Sort (max1?u.4550)
DecidableRel
α: Type ?u.4504
α
(· < ·): ααProp
(· < ·)
] [
IsTotal: (α : Type ?u.4577) → (ααProp) → Prop
IsTotal
α: Type ?u.4504
α
(· ≤ ·): ααProp
(· ≤ ·)
] :
LinearOrder: Type ?u.4596 → Type ?u.4596
LinearOrder
(
Antisymmetrization: (α : Type ?u.4597) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.4597
Antisymmetrization
α: Type ?u.4504
α
(· ≤ ·): ααProp
(· ≤ ·)
) := {
instPartialOrderAntisymmetrizationLeToLEInstIsPreorderLeToLE: {α : Type ?u.4650} → [inst : Preorder α] → PartialOrder (Antisymmetrization α fun x x_1 => x x_1)
instPartialOrderAntisymmetrizationLeToLEInstIsPreorderLeToLE
with le_total := fun
a: ?m.4746
a
b: ?m.4749
b
=>
Quotient.inductionOn₂': ∀ {α : Sort ?u.4751} {β : Sort ?u.4752} {s₁ : Setoid α} {s₂ : Setoid β} {p : Quotient s₁Quotient s₂Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂), (∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) → p q₁ q₂
Quotient.inductionOn₂'
a: ?m.4746
a
b: ?m.4749
b
<|
total_of: ∀ {α : Type ?u.5153} (r : ααProp) [inst : IsTotal α r] (a b : α), r a b r b a
total_of
(· ≤ ·): ααProp
(· ≤ ·)
, decidableLE := fun
_: ?m.4808
_
_: ?m.4811
_
=> show
Decidable: PropType
Decidable
(
Quotient.liftOn₂': {α : Sort ?u.4816} → {β : Sort ?u.4815} → {γ : Sort ?u.4814} → {s₁ : Setoid α} → {s₂ : Setoid β} → Quotient s₁Quotient s₂(f : αβγ) → (∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), Setoid.r a₁ b₁Setoid.r a₂ b₂f a₁ a₂ = f b₁ b₂) → γ
Quotient.liftOn₂'
_: Quotient ?m.4820
_
_: Quotient ?m.4821
_
_: ?m.4817?m.4818?m.4819
_
_: ∀ (a₁ : ?m.4817) (a₂ : ?m.4818) (b₁ : ?m.4817) (b₂ : ?m.4818), Setoid.r a₁ b₁Setoid.r a₂ b₂?m.4824 a₁ a₂ = ?m.4824 b₁ b₂
_
) from
inferInstance: {α : Sort ?u.4859} → [i : α] → α
inferInstance
, decidableLT := fun
_: ?m.5006
_
_: ?m.5009
_
=> show
Decidable: PropType
Decidable
(
Quotient.liftOn₂': {α : Sort ?u.5014} → {β : Sort ?u.5013} → {γ : Sort ?u.5012} → {s₁ : Setoid α} → {s₂ : Setoid β} → Quotient s₁Quotient s₂(f : αβγ) → (∀ (a₁ : α) (a₂ : β) (b₁ : α) (b₂ : β), Setoid.r a₁ b₁Setoid.r a₂ b₂f a₁ a₂ = f b₁ b₂) → γ
Quotient.liftOn₂'
_: Quotient ?m.5018
_
_: Quotient ?m.5019
_
_: ?m.5015?m.5016?m.5017
_
_: ∀ (a₁ : ?m.5015) (a₂ : ?m.5016) (b₁ : ?m.5015) (b₂ : ?m.5016), Setoid.r a₁ b₁Setoid.r a₂ b₂?m.5022 a₁ a₂ = ?m.5022 b₁ b₂
_
) from
inferInstance: {α : Sort ?u.5036} → [i : α] → α
inferInstance
} @[simp] theorem
toAntisymmetrization_le_toAntisymmetrization_iff: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, toAntisymmetrization (fun x x_1 => x x_1) a toAntisymmetrization (fun x x_1 => x x_1) b a b
toAntisymmetrization_le_toAntisymmetrization_iff
: @
toAntisymmetrization: {α : Type ?u.6400} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
α: Type ?u.6383
α
(· ≤ ·): ααProp
(· ≤ ·)
_
a: α
a
≤ @
toAntisymmetrization: {α : Type ?u.6446} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
α: Type ?u.6383
α
(· ≤ ·): ααProp
(· ≤ ·)
_
b: α
b
a: α
a
b: α
b
:=
Iff.rfl: ∀ {a : Prop}, a a
Iff.rfl
#align to_antisymmetrization_le_to_antisymmetrization_iff
toAntisymmetrization_le_toAntisymmetrization_iff: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, toAntisymmetrization (fun x x_1 => x x_1) a toAntisymmetrization (fun x x_1 => x x_1) b a b
toAntisymmetrization_le_toAntisymmetrization_iff
@[simp] theorem
toAntisymmetrization_lt_toAntisymmetrization_iff: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, toAntisymmetrization (fun x x_1 => x x_1) a < toAntisymmetrization (fun x x_1 => x x_1) b a < b
toAntisymmetrization_lt_toAntisymmetrization_iff
: @
toAntisymmetrization: {α : Type ?u.6558} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
α: Type ?u.6541
α
(· ≤ ·): ααProp
(· ≤ ·)
_
a: α
a
< @
toAntisymmetrization: {α : Type ?u.6604} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
α: Type ?u.6541
α
(· ≤ ·): ααProp
(· ≤ ·)
_
b: α
b
a: α
a
<
b: α
b
:=
Iff.rfl: ∀ {a : Prop}, a a
Iff.rfl
#align to_antisymmetrization_lt_to_antisymmetrization_iff
toAntisymmetrization_lt_toAntisymmetrization_iff: ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, toAntisymmetrization (fun x x_1 => x x_1) a < toAntisymmetrization (fun x x_1 => x x_1) b a < b
toAntisymmetrization_lt_toAntisymmetrization_iff
@[simp] theorem
ofAntisymmetrization_le_ofAntisymmetrization_iff: ∀ {α : Type u_1} [inst : Preorder α] {a b : Antisymmetrization α fun x x_1 => x x_1}, ofAntisymmetrization (fun x x_1 => x x_1) a ofAntisymmetrization (fun x x_1 => x x_1) b a b
ofAntisymmetrization_le_ofAntisymmetrization_iff
{
a: Antisymmetrization α fun x x_1 => x x_1
a
b: Antisymmetrization α fun x x_1 => x x_1
b
:
Antisymmetrization: (α : Type ?u.6770) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.6770
Antisymmetrization
α: Type ?u.6706
α
(· ≤ ·): ααProp
(· ≤ ·)
} :
ofAntisymmetrization: {α : Type ?u.6786} → (r : ααProp) → [inst : IsPreorder α r] → Antisymmetrization α rα
ofAntisymmetrization
(· ≤ ·): ααProp
(· ≤ ·)
a: Antisymmetrization α fun x x_1 => x x_1
a
ofAntisymmetrization: {α : Type ?u.6898} → (r : ααProp) → [inst : IsPreorder α r] → Antisymmetrization α rα
ofAntisymmetrization
(· ≤ ·): ααProp
(· ≤ ·)
b: Antisymmetrization α fun x x_1 => x x_1
b
a: Antisymmetrization α fun x x_1 => x x_1
a
b: Antisymmetrization α fun x x_1 => x x_1
b
:= (
Quotient.out'RelEmbedding: {α : Type ?u.7001} → {x : Setoid α} → {r : ααProp} → (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) → (fun a b => Quotient.liftOn₂' a b r H) ↪r r
Quotient.out'RelEmbedding
_: ∀ (a₁ b₁ a₂ b₂ : ?m.7002), a₁ a₂b₁ b₂?m.7004 a₁ b₁ = ?m.7004 a₂ b₂
_
).
map_rel_iff: ∀ {α : Type ?u.7006} {β : Type ?u.7007} {r : ααProp} {s : ββProp} (f : r ↪r s) {a b : α}, s (f a) (f b) r a b
map_rel_iff
#align of_antisymmetrization_le_of_antisymmetrization_iff
ofAntisymmetrization_le_ofAntisymmetrization_iff: ∀ {α : Type u_1} [inst : Preorder α] {a b : Antisymmetrization α fun x x_1 => x x_1}, ofAntisymmetrization (fun x x_1 => x x_1) a ofAntisymmetrization (fun x x_1 => x x_1) b a b
ofAntisymmetrization_le_ofAntisymmetrization_iff
@[simp] theorem
ofAntisymmetrization_lt_ofAntisymmetrization_iff: ∀ {α : Type u_1} [inst : Preorder α] {a b : Antisymmetrization α fun x x_1 => x x_1}, ofAntisymmetrization (fun x x_1 => x x_1) a < ofAntisymmetrization (fun x x_1 => x x_1) b a < b
ofAntisymmetrization_lt_ofAntisymmetrization_iff
{
a: Antisymmetrization α fun x x_1 => x x_1
a
b: Antisymmetrization α fun x x_1 => x x_1
b
:
Antisymmetrization: (α : Type ?u.7197) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.7197
Antisymmetrization
α: Type ?u.7133
α
(· ≤ ·): ααProp
(· ≤ ·)
} :
ofAntisymmetrization: {α : Type ?u.7213} → (r : ααProp) → [inst : IsPreorder α r] → Antisymmetrization α rα
ofAntisymmetrization
(· ≤ ·): ααProp
(· ≤ ·)
a: Antisymmetrization α fun x x_1 => x x_1
a
<
ofAntisymmetrization: {α : Type ?u.7325} → (r : ααProp) → [inst : IsPreorder α r] → Antisymmetrization α rα
ofAntisymmetrization
(· ≤ ·): ααProp
(· ≤ ·)
b: Antisymmetrization α fun x x_1 => x x_1
b
a: Antisymmetrization α fun x x_1 => x x_1
a
<
b: Antisymmetrization α fun x x_1 => x x_1
b
:= (
Quotient.out'RelEmbedding: {α : Type ?u.7435} → {x : Setoid α} → {r : ααProp} → (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) → (fun a b => Quotient.liftOn₂' a b r H) ↪r r
Quotient.out'RelEmbedding
_: ∀ (a₁ b₁ a₂ b₂ : ?m.7436), a₁ a₂b₁ b₂?m.7438 a₁ b₁ = ?m.7438 a₂ b₂
_
).
map_rel_iff: ∀ {α : Type ?u.7440} {β : Type ?u.7441} {r : ααProp} {s : ββProp} (f : r ↪r s) {a b : α}, s (f a) (f b) r a b
map_rel_iff
#align of_antisymmetrization_lt_of_antisymmetrization_iff
ofAntisymmetrization_lt_ofAntisymmetrization_iff: ∀ {α : Type u_1} [inst : Preorder α] {a b : Antisymmetrization α fun x x_1 => x x_1}, ofAntisymmetrization (fun x x_1 => x x_1) a < ofAntisymmetrization (fun x x_1 => x x_1) b a < b
ofAntisymmetrization_lt_ofAntisymmetrization_iff
@[mono] theorem
toAntisymmetrization_mono: ∀ {α : Type u_1} [inst : Preorder α], Monotone (toAntisymmetrization fun x x_1 => x x_1)
toAntisymmetrization_mono
:
Monotone: {α : Type ?u.7584} → {β : Type ?u.7583} → [inst : Preorder α] → [inst : Preorder β] → (αβ) → Prop
Monotone
(@
toAntisymmetrization: {α : Type ?u.7615} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
α: Type ?u.7567
α
(· ≤ ·): ααProp
(· ≤ ·)
_) := fun
_: ?m.7693
_
_: ?m.7696
_
=>
id: ∀ {α : Sort ?u.7698}, αα
id
#align to_antisymmetrization_mono
toAntisymmetrization_mono: ∀ {α : Type u_1} [inst : Preorder α], Monotone (toAntisymmetrization fun x x_1 => x x_1)
toAntisymmetrization_mono
private theorem
lift_fun_antisymmRel: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), (Setoid.r Setoid.r) f f
lift_fun_antisymmRel
(
f: α →o β
f
:
α: Type ?u.7713
α
→o
β: Type ?u.7716
β
) : ((
AntisymmRel.setoid: (α : Type ?u.7751) → (r : ααProp) → [inst : IsPreorder α r] → Setoid α
AntisymmRel.setoid
α: Type ?u.7713
α
(· ≤ ·): ααProp
(· ≤ ·)
).
r: {α : Sort ?u.7793} → [self : Setoid α] → ααProp
r
⇒ (
AntisymmRel.setoid: (α : Type ?u.7802) → (r : ααProp) → [inst : IsPreorder α r] → Setoid α
AntisymmRel.setoid
β: Type ?u.7716
β
(· ≤ ·): ββProp
(· ≤ ·)
).
r: {α : Sort ?u.7844} → [self : Setoid α] → ααProp
r
)
f: α →o β
f
f: α →o β
f
:= fun
_: ?m.7927
_
_: ?m.7930
_
h: ?m.7933
h
=> ⟨
f: α →o β
f
.
mono: ∀ {α : Type ?u.7945} {β : Type ?u.7946} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), Monotone f
mono
h: ?m.7933
h
.
1: ∀ {a b : Prop}, a ba
1
,
f: α →o β
f
.
mono: ∀ {α : Type ?u.7987} {β : Type ?u.7988} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), Monotone f
mono
h: ?m.7933
h
.
2: ∀ {a b : Prop}, a bb
2
⟩ /-- 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: (α →o β) → (Antisymmetrization α fun x x_1 => x x_1) →o Antisymmetrization β fun x x_1 => x x_1
OrderHom.antisymmetrization
(
f: α →o β
f
:
α: Type ?u.8024
α
→o
β: Type ?u.8027
β
) :
Antisymmetrization: (α : Type ?u.8056) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.8056
Antisymmetrization
α: Type ?u.8024
α
(· ≤ ·): ααProp
(· ≤ ·)
→o
Antisymmetrization: (α : Type ?u.8098) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.8098
Antisymmetrization
β: Type ?u.8027
β
(· ≤ ·): ββProp
(· ≤ ·)
:= ⟨
Quotient.map': {α : Sort ?u.8233} → {β : Sort ?u.8232} → {s₁ : Setoid α} → {s₂ : Setoid β} → (f : αβ) → (Setoid.r Setoid.r) f fQuotient s₁Quotient s₂
Quotient.map'
f: α →o β
f
<|
lift_fun_antisymmRel: ∀ {α : Type ?u.8283} {β : Type ?u.8284} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), (Setoid.r Setoid.r) f f
lift_fun_antisymmRel
f: α →o β
f
, fun
a: ?m.8311
a
b: ?m.8314
b
=>
Quotient.inductionOn₂': ∀ {α : Sort ?u.8316} {β : Sort ?u.8317} {s₁ : Setoid α} {s₂ : Setoid β} {p : Quotient s₁Quotient s₂Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂), (∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) → p q₁ q₂
Quotient.inductionOn₂'
a: ?m.8311
a
b: ?m.8314
b
<|
f: α →o β
f
.
mono: ∀ {α : Type ?u.8370} {β : Type ?u.8371} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), Monotone f
mono
#align order_hom.antisymmetrization
OrderHom.antisymmetrization: {α : Type u_1} → {β : Type u_2} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → (Antisymmetrization α fun x x_1 => x x_1) →o Antisymmetrization β fun x x_1 => x x_1
OrderHom.antisymmetrization
@[simp] theorem
OrderHom.coe_antisymmetrization: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), ↑(OrderHom.antisymmetrization f) = Quotient.map' f (_ : (Setoid.r Setoid.r) f f)
OrderHom.coe_antisymmetrization
(
f: α →o β
f
:
α: Type ?u.8484
α
→o
β: Type ?u.8487
β
) : ⇑
f: α →o β
f
.
antisymmetrization: {α : Type ?u.8516} → {β : Type ?u.8515} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → (Antisymmetrization α fun x x_1 => x x_1) →o Antisymmetrization β fun x x_1 => x x_1
antisymmetrization
=
Quotient.map': {α : Sort ?u.8580} → {β : Sort ?u.8579} → {s₁ : Setoid α} → {s₂ : Setoid β} → (f : αβ) → (Setoid.r Setoid.r) f fQuotient s₁Quotient s₂
Quotient.map'
f: α →o β
f
(
lift_fun_antisymmRel: ∀ {α : Type ?u.8614} {β : Type ?u.8615} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), (Setoid.r Setoid.r) f f
lift_fun_antisymmRel
f: α →o β
f
) :=
rfl: ∀ {α : Sort ?u.8652} {a : α}, a = a
rfl
#align order_hom.coe_antisymmetrization
OrderHom.coe_antisymmetrization: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), ↑(OrderHom.antisymmetrization f) = Quotient.map' f (_ : (Setoid.r Setoid.r) f f)
OrderHom.coe_antisymmetrization
/- Porting notes: Removed @[simp] attribute. With this `simp` lemma the LHS of `OrderHom.antisymmetrization_apply_mk` is not in normal-form -/ theorem
OrderHom.antisymmetrization_apply: ∀ (f : α →o β) (a : Antisymmetrization α fun x x_1 => x x_1), ↑(OrderHom.antisymmetrization f) a = Quotient.map' f (_ : (Setoid.r Setoid.r) f f) a
OrderHom.antisymmetrization_apply
(
f: α →o β
f
:
α: Type ?u.8685
α
→o
β: Type ?u.8688
β
) (
a: Antisymmetrization α fun x x_1 => x x_1
a
:
Antisymmetrization: (α : Type ?u.8715) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.8715
Antisymmetrization
α: Type ?u.8685
α
(· ≤ ·): ααProp
(· ≤ ·)
) :
f: α →o β
f
.
antisymmetrization: {α : Type ?u.8761} → {β : Type ?u.8760} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → (Antisymmetrization α fun x x_1 => x x_1) →o Antisymmetrization β fun x x_1 => x x_1
antisymmetrization
a: Antisymmetrization α fun x x_1 => x x_1
a
=
Quotient.map': {α : Sort ?u.8829} → {β : Sort ?u.8828} → {s₁ : Setoid α} → {s₂ : Setoid β} → (f : αβ) → (Setoid.r Setoid.r) f fQuotient s₁Quotient s₂
Quotient.map'
f: α →o β
f
(
lift_fun_antisymmRel: ∀ {α : Type ?u.8863} {β : Type ?u.8864} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), (Setoid.r Setoid.r) f f
lift_fun_antisymmRel
f: α →o β
f
)
a: Antisymmetrization α fun x x_1 => x x_1
a
:=
rfl: ∀ {α : Sort ?u.8897} {a : α}, a = a
rfl
#align order_hom.antisymmetrization_apply
OrderHom.antisymmetrization_apply: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (a : Antisymmetrization α fun x x_1 => x x_1), ↑(OrderHom.antisymmetrization f) a = Quotient.map' f (_ : (Setoid.r Setoid.r) f f) a
OrderHom.antisymmetrization_apply
@[simp] theorem
OrderHom.antisymmetrization_apply_mk: ∀ (f : α →o β) (a : α), ↑(OrderHom.antisymmetrization f) (toAntisymmetrization (fun x x_1 => x x_1) a) = toAntisymmetrization (fun x x_1 => x x_1) (f a)
OrderHom.antisymmetrization_apply_mk
(
f: α →o β
f
:
α: Type ?u.8916
α
→o
β: Type ?u.8919
β
) (
a: α
a
:
α: Type ?u.8916
α
) :
f: α →o β
f
.
antisymmetrization: {α : Type ?u.8950} → {β : Type ?u.8949} → [inst : Preorder α] → [inst_1 : Preorder β] → (α →o β) → (Antisymmetrization α fun x x_1 => x x_1) →o Antisymmetrization β fun x x_1 => x x_1
antisymmetrization
(
toAntisymmetrization: {α : Type ?u.9013} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
_: ?m.9014?m.9014Prop
_
a: α
a
) =
toAntisymmetrization: {α : Type ?u.9059} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
_: ?m.9060?m.9060Prop
_
(
f: α →o β
f
a: α
a
) := @
Quotient.map_mk: ∀ {α : Sort ?u.9194} {β : Sort ?u.9195} [sa : Setoid α] [sb : Setoid β] (f : αβ) (h : ((fun x x_1 => x x_1) fun x x_1 => x x_1) f f) (x : α), Quotient.map f h (Quotient.mk sa x) = Quotient.mk sb (f x)
Quotient.map_mk
_: Sort ?u.9194
_
_: Sort ?u.9195
_
(
_root_.id: {α : Sort ?u.9198} → αα
_root_.id
_: ?m.9199
_
) (
_root_.id: {α : Sort ?u.9201} → αα
_root_.id
_: ?m.9202
_
)
f: α →o β
f
(
lift_fun_antisymmRel: ∀ {α : Type ?u.9245} {β : Type ?u.9246} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β), (Setoid.r Setoid.r) f f
lift_fun_antisymmRel
f: α →o β
f
)
_: ?m.9196
_
#align order_hom.antisymmetrization_apply_mk
OrderHom.antisymmetrization_apply_mk: ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (f : α →o β) (a : α), ↑(OrderHom.antisymmetrization f) (toAntisymmetrization (fun x x_1 => x x_1) a) = toAntisymmetrization (fun x x_1 => x x_1) (f a)
OrderHom.antisymmetrization_apply_mk
variable (
α: ?m.9367
α
) /-- `ofAntisymmetrization` as an order embedding. -/ @[
simps: ∀ (α : Type u_1) [inst : Preorder α] (a : Antisymmetrization α fun x x_1 => x x_1), ↑(ofAntisymmetrization α) a = _root_.ofAntisymmetrization (fun x x_1 => x x_1) a
simps
] noncomputable def
OrderEmbedding.ofAntisymmetrization: (α : Type u_1) → [inst : Preorder α] → (Antisymmetrization α fun x x_1 => x x_1) ↪o α
OrderEmbedding.ofAntisymmetrization
:
Antisymmetrization: (α : Type ?u.9388) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.9388
Antisymmetrization
α: Type ?u.9370
α
(· ≤ ·): ααProp
(· ≤ ·)
↪o
α: Type ?u.9370
α
:= {
Quotient.out'RelEmbedding: {α : Type ?u.9465} → {x : Setoid α} → {r : ααProp} → (H : ∀ (a₁ b₁ a₂ b₂ : α), a₁ a₂b₁ b₂r a₁ b₁ = r a₂ b₂) → (fun a b => Quotient.liftOn₂' a b r H) ↪r r
Quotient.out'RelEmbedding
_: ∀ (a₁ b₁ a₂ b₂ : ?m.9466), a₁ a₂b₁ b₂?m.9468 a₁ b₁ = ?m.9468 a₂ b₂
_
with toFun :=
_root_.ofAntisymmetrization: {α : Type ?u.9499} → (r : ααProp) → [inst : IsPreorder α r] → Antisymmetrization α rα
_root_.ofAntisymmetrization
_: ?m.9500?m.9500Prop
_
} #align order_embedding.of_antisymmetrization
OrderEmbedding.ofAntisymmetrization: (α : Type u_1) → [inst : Preorder α] → (Antisymmetrization α fun x x_1 => x x_1) ↪o α
OrderEmbedding.ofAntisymmetrization
#align order_embedding.of_antisymmetrization_apply
OrderEmbedding.ofAntisymmetrization_apply: ∀ (α : Type u_1) [inst : Preorder α] (a : Antisymmetrization α fun x x_1 => x x_1), ↑(OrderEmbedding.ofAntisymmetrization α) a = ofAntisymmetrization (fun x x_1 => x x_1) a
OrderEmbedding.ofAntisymmetrization_apply
/-- `Antisymmetrization` and `orderDual` commute. -/ def
OrderIso.dualAntisymmetrization: (Antisymmetrization α fun x x_1 => x x_1)ᵒᵈ ≃o Antisymmetrization αᵒᵈ fun x x_1 => x x_1
OrderIso.dualAntisymmetrization
: (
Antisymmetrization: (α : Type ?u.9744) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.9744
Antisymmetrization
α: Type ?u.9725
α
(· ≤ ·): ααProp
(· ≤ ·)
)ᵒᵈ ≃o
Antisymmetrization: (α : Type ?u.9790) → (r : ααProp) → [inst : IsPreorder α r] → Type ?u.9790
Antisymmetrization
α: Type ?u.9725
α
ᵒᵈ
(· ≤ ·): αᵒᵈαᵒᵈProp
(· ≤ ·)
where toFun := (
Quotient.map': {α : Sort ?u.9942} → {β : Sort ?u.9941} → {s₁ : Setoid α} → {s₂ : Setoid β} → (f : αβ) → (Setoid.r Setoid.r) f fQuotient s₁Quotient s₂
Quotient.map'
id: {α : Sort ?u.9947} → αα
id
) fun
_: ?m.9966
_
_: ?m.9969
_
=>
And.symm: ∀ {a b : Prop}, a bb a
And.symm
invFun := (
Quotient.map': {α : Sort ?u.9993} → {β : Sort ?u.9992} → {s₁ : Setoid α} → {s₂ : Setoid β} → (f : αβ) → (Setoid.r Setoid.r) f fQuotient s₁Quotient s₂
Quotient.map'
id: {α : Sort ?u.9998} → αα
id
) fun
_: ?m.10008
_
_: ?m.10011
_
=>
And.symm: ∀ {a b : Prop}, a bb a
And.symm
left_inv
a: ?m.10031
a
:=
Quotient.inductionOn': ∀ {α : Sort ?u.10033} {s₁ : Setoid α} {p : Quotient s₁Prop} (q : Quotient s₁), (∀ (a : α), p (Quotient.mk'' a)) → p q
Quotient.inductionOn'
a: ?m.10031
a
fun
a: ?m.10167
a
=>

Goals accomplished! 🐙
α: Type ?u.9725

β: Type ?u.9728

inst✝¹: Preorder α

inst✝: Preorder β

a✝¹, b: α

a✝: (Antisymmetrization α fun x x_1 => x x_1)ᵒᵈ

a: α


Quotient.map' id (_ : ∀ (x x_1 : αᵒᵈ), (fun x x_2 => x x_2) x x_1 (fun x x_2 => x x_2) x_1 x(fun x x_2 => x x_2) x_1 x (fun x x_2 => x x_2) x x_1) (Quotient.map' id (_ : ∀ (x x_1 : α), (fun x x_2 => x x_2) x x_1 (fun x x_2 => x x_2) x_1 x(fun x x_2 => x x_2) x_1 x (fun x x_2 => x x_2) x x_1) (Quotient.mk'' a)) = Quotient.mk'' a
α: Type ?u.9725

β: Type ?u.9728

inst✝¹: Preorder α

inst✝: Preorder β

a✝¹, b: α

a✝: (Antisymmetrization α fun x x_1 => x x_1)ᵒᵈ

a: α


Quotient.map' id (_ : ∀ (x x_1 : αᵒᵈ), (fun x x_2 => x x_2) x x_1 (fun x x_2 => x x_2) x_1 x(fun x x_2 => x x_2) x_1 x (fun x x_2 => x x_2) x x_1) (Quotient.map' id (_ : ∀ (x x_1 : α), (fun x x_2 => x x_2) x x_1 (fun x x_2 => x x_2) x_1 x(fun x x_2 => x x_2) x_1 x (fun x x_2 => x x_2) x x_1) (Quotient.mk'' a)) = Quotient.mk'' a
α: Type ?u.9725

β: Type ?u.9728

inst✝¹: Preorder α

inst✝: Preorder β

a✝¹, b: α

a✝: (Antisymmetrization α fun x x_1 => x x_1)ᵒᵈ

a: α


α: Type ?u.9725

β: Type ?u.9728

inst✝¹: Preorder α

inst✝: Preorder β

a✝¹, b: α

a✝: (Antisymmetrization α fun x x_1 => x x_1)ᵒᵈ

a: α


Quotient.map' id (_ : ∀ (x x_1 : αᵒᵈ), (fun x x_2 => x x_2) x x_1 (fun x x_2 => x x_2) x_1 x(fun x x_2 => x x_2) x_1 x (fun x x_2 => x x_2) x x_1) (Quotient.map' id (_ : ∀ (x x_1 : α), (fun x x_2 => x x_2) x x_1 (fun x x_2 => x x_2) x_1 x(fun x x_2 => x x_2) x_1 x (fun x x_2 => x x_2) x x_1) (Quotient.mk'' a)) = Quotient.mk'' a

Goals accomplished! 🐙

Goals accomplished! 🐙
right_inv
a: ?m.10069
a
:=
Quotient.inductionOn': ∀ {α : Sort ?u.10071} {s₁ : Setoid α} {p : Quotient s₁Prop} (q : Quotient s₁), (∀ (a : α), p (Quotient.mk'' a)) → p q
Quotient.inductionOn'
a: ?m.10069
a
fun
a: ?m.10173
a
=>

Goals accomplished! 🐙
α: Type ?u.9725

β: Type ?u.9728

inst✝¹: Preorder α

inst✝: Preorder β

a✝¹, b: α

a✝: Antisymmetrization αᵒᵈ fun x x_1 => x x_1

a: αᵒᵈ


Quotient.map' id (_ : ∀ (x x_1 : α), (fun x x_2 => x x_2) x x_1 (fun x x_2 => x x_2) x_1 x(fun x x_2 => x x_2) x_1 x (fun x x_2 => x x_2) x x_1) (Quotient.map' id (_ : ∀ (x x_1 : αᵒᵈ), (fun x x_2 => x x_2) x x_1 (fun x x_2 => x x_2) x_1 x(fun x x_2 => x x_2) x_1 x (fun x x_2 => x x_2) x x_1) (Quotient.mk'' a)) = Quotient.mk'' a
α: Type ?u.9725

β: Type ?u.9728

inst✝¹: Preorder α

inst✝: Preorder β

a✝¹, b: α

a✝: Antisymmetrization αᵒᵈ fun x x_1 => x x_1

a: αᵒᵈ


Quotient.map' id (_ : ∀ (x x_1 : α), (fun x x_2 => x x_2) x x_1 (fun x x_2 => x x_2) x_1 x(fun x x_2 => x x_2) x_1 x (fun x x_2 => x x_2) x x_1) (Quotient.map' id (_ : ∀ (x x_1 : αᵒᵈ), (fun x x_2 => x x_2) x x_1 (fun x x_2 => x x_2) x_1 x(fun x x_2 => x x_2) x_1 x (fun x x_2 => x x_2) x x_1) (Quotient.mk'' a)) = Quotient.mk'' a
α: Type ?u.9725

β: Type ?u.9728

inst✝¹: Preorder α

inst✝: Preorder β

a✝¹, b: α

a✝: Antisymmetrization αᵒᵈ fun x x_1 => x x_1

a: αᵒᵈ


α: Type ?u.9725

β: Type ?u.9728

inst✝¹: Preorder α

inst✝: Preorder β

a✝¹, b: α

a✝: Antisymmetrization αᵒᵈ fun x x_1 => x x_1

a: αᵒᵈ


Quotient.map' id (_ : ∀ (x x_1 : α), (fun x x_2 => x x_2) x x_1 (fun x x_2 => x x_2) x_1 x(fun x x_2 => x x_2) x_1 x (fun x x_2 => x x_2) x x_1) (Quotient.map' id (_ : ∀ (x x_1 : αᵒᵈ), (fun x x_2 => x x_2) x x_1 (fun x x_2 => x x_2) x_1 x(fun x x_2 => x x_2) x_1 x (fun x x_2 => x x_2) x x_1) (Quotient.mk'' a)) = Quotient.mk'' a

Goals accomplished! 🐙

Goals accomplished! 🐙
map_rel_iff' := @fun
a: ?m.10102
a
b: ?m.10105
b
=>
Quotient.inductionOn₂': ∀ {α : Sort ?u.10107} {β : Sort ?u.10108} {s₁ : Setoid α} {s₂ : Setoid β} {p : Quotient s₁Quotient s₂Prop} (q₁ : Quotient s₁) (q₂ : Quotient s₂), (∀ (a₁ : α) (a₂ : β), p (Quotient.mk'' a₁) (Quotient.mk'' a₂)) → p q₁ q₂
Quotient.inductionOn₂'
a: ?m.10102
a
b: ?m.10105
b
fun
a: ?m.10179
a
b: ?m.10182
b
=>
Iff.rfl: ∀ {a : Prop}, a a
Iff.rfl
#align order_iso.dual_antisymmetrization
OrderIso.dualAntisymmetrization: (α : Type u_1) → [inst : Preorder α] → (Antisymmetrization α fun x x_1 => x x_1)ᵒᵈ ≃o Antisymmetrization αᵒᵈ fun x x_1 => x x_1
OrderIso.dualAntisymmetrization
@[simp] theorem
OrderIso.dualAntisymmetrization_apply: ∀ (α : Type u_1) [inst : Preorder α] (a : α), ↑(dualAntisymmetrization α) (toDual (toAntisymmetrization (fun x x_1 => x x_1) a)) = toAntisymmetrization (fun x x_1 => x x_1) (toDual a)
OrderIso.dualAntisymmetrization_apply
(
a: α
a
:
α: Type ?u.10973
α
) :
OrderIso.dualAntisymmetrization: (α : Type ?u.10992) → [inst : Preorder α] → (Antisymmetrization α fun x x_1 => x x_1)ᵒᵈ ≃o Antisymmetrization αᵒᵈ fun x x_1 => x x_1
OrderIso.dualAntisymmetrization
_: Type ?u.10992
_
(
toDual: {α : Type ?u.11100} → α αᵒᵈ
toDual
<|
toAntisymmetrization: {α : Type ?u.11166} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
_: ?m.11167?m.11167Prop
_
a: α
a
) =
toAntisymmetrization: {α : Type ?u.11240} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
_: ?m.11241?m.11241Prop
_
(
toDual: {α : Type ?u.11244} → α αᵒᵈ
toDual
a: α
a
) :=
rfl: ∀ {α : Sort ?u.11418} {a : α}, a = a
rfl
#align order_iso.dual_antisymmetrization_apply
OrderIso.dualAntisymmetrization_apply: ∀ (α : Type u_1) [inst : Preorder α] (a : α), ↑(OrderIso.dualAntisymmetrization α) (toDual (toAntisymmetrization (fun x x_1 => x x_1) a)) = toAntisymmetrization (fun x x_1 => x x_1) (toDual a)
OrderIso.dualAntisymmetrization_apply
@[simp] theorem
OrderIso.dualAntisymmetrization_symm_apply: ∀ (α : Type u_1) [inst : Preorder α] (a : α), ↑(symm (dualAntisymmetrization α)) (toAntisymmetrization (fun x x_1 => x x_1) (toDual a)) = toDual (toAntisymmetrization (fun x x_1 => x x_1) a)
OrderIso.dualAntisymmetrization_symm_apply
(
a: α
a
:
α: Type ?u.11489
α
) : (
OrderIso.dualAntisymmetrization: (α : Type ?u.11508) → [inst : Preorder α] → (Antisymmetrization α fun x x_1 => x x_1)ᵒᵈ ≃o Antisymmetrization αᵒᵈ fun x x_1 => x x_1
OrderIso.dualAntisymmetrization
_: Type ?u.11508
_
).
symm: {α : Type ?u.11525} → {β : Type ?u.11524} → [inst : LE α] → [inst_1 : LE β] → α ≃o ββ ≃o α
symm
(
toAntisymmetrization: {α : Type ?u.11739} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
_: ?m.11740?m.11740Prop
_
<|
toDual: {α : Type ?u.11776} → α αᵒᵈ
toDual
a: α
a
) =
toDual: {α : Type ?u.11949} → α αᵒᵈ
toDual
(
toAntisymmetrization: {α : Type ?u.12015} → (r : ααProp) → [inst : IsPreorder α r] → αAntisymmetrization α r
toAntisymmetrization
_: ?m.12016?m.12016Prop
_
a: α
a
) :=
rfl: ∀ {α : Sort ?u.12123} {a : α}, a = a
rfl
#align order_iso.dual_antisymmetrization_symm_apply
OrderIso.dualAntisymmetrization_symm_apply: ∀ (α : Type u_1) [inst : Preorder α] (a : α), ↑(OrderIso.symm (OrderIso.dualAntisymmetrization α)) (toAntisymmetrization (fun x x_1 => x x_1) (toDual a)) = toDual (toAntisymmetrization (fun x x_1 => x x_1) a)
OrderIso.dualAntisymmetrization_symm_apply
end Preorder