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) 2017 Mario Carneiro. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro

! This file was ported from Lean 3 source module order.rel_iso.group
! leanprover-community/mathlib commit 62a5626868683c104774de8d85b9855234ac807c
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Algebra.Group.Defs
import Mathlib.Order.RelIso.Basic

/-!
# Relation isomorphisms form a group
-/


variable {
Ī±: Type ?u.11
Ī±
:
Type _: Type (?u.2929+1)
Type _
} {
r: Ī± ā†’ Ī± ā†’ Prop
r
:
Ī±: Type ?u.2
Ī±
ā†’
Ī±: Type ?u.2
Ī±
ā†’
Prop: Type
Prop
} namespace RelIso
instance: {Ī± : Type u_1} ā†’ {r : Ī± ā†’ Ī± ā†’ Prop} ā†’ Group (r ā‰ƒr r)
instance
:
Group: Type ?u.20 ā†’ Type ?u.20
Group
(
r: Ī± ā†’ Ī± ā†’ Prop
r
ā‰ƒr
r: Ī± ā†’ Ī± ā†’ Prop
r
) where one :=
RelIso.refl: {Ī± : Type ?u.191} ā†’ (r : Ī± ā†’ Ī± ā†’ Prop) ā†’ r ā‰ƒr r
RelIso.refl
r: Ī± ā†’ Ī± ā†’ Prop
r
mul
fā‚: ?m.54
fā‚
fā‚‚: ?m.57
fā‚‚
:=
fā‚‚: ?m.57
fā‚‚
.
trans: {Ī± : Type ?u.61} ā†’ {Ī² : Type ?u.60} ā†’ {Ī³ : Type ?u.59} ā†’ {r : Ī± ā†’ Ī± ā†’ Prop} ā†’ {s : Ī² ā†’ Ī² ā†’ Prop} ā†’ {t : Ī³ ā†’ Ī³ ā†’ Prop} ā†’ r ā‰ƒr s ā†’ s ā‰ƒr t ā†’ r ā‰ƒr t
trans
fā‚: ?m.54
fā‚
inv :=
RelIso.symm: {Ī± : Type ?u.273} ā†’ {Ī² : Type ?u.272} ā†’ {r : Ī± ā†’ Ī± ā†’ Prop} ā†’ {s : Ī² ā†’ Ī² ā†’ Prop} ā†’ r ā‰ƒr s ā†’ s ā‰ƒr r
RelIso.symm
mul_assoc
fā‚: ?m.95
fā‚
fā‚‚: ?m.98
fā‚‚
fā‚ƒ: ?m.101
fā‚ƒ
:=
rfl: āˆ€ {Ī± : Sort ?u.103} {a : Ī±}, a = a
rfl
one_mul
f: ?m.200
f
:=
ext: āˆ€ {Ī± : Type ?u.202} {Ī² : Type ?u.203} {r : Ī± ā†’ Ī± ā†’ Prop} {s : Ī² ā†’ Ī² ā†’ Prop} ā¦ƒf g : r ā‰ƒr sā¦„, (āˆ€ (x : Ī±), ā†‘f x = ā†‘g x) ā†’ f = g
ext
fun
_: ?m.223
_
=>
rfl: āˆ€ {Ī± : Sort ?u.225} {a : Ī±}, a = a
rfl
mul_one
f: ?m.233
f
:=
ext: āˆ€ {Ī± : Type ?u.235} {Ī² : Type ?u.236} {r : Ī± ā†’ Ī± ā†’ Prop} {s : Ī² ā†’ Ī² ā†’ Prop} ā¦ƒf g : r ā‰ƒr sā¦„, (āˆ€ (x : Ī±), ā†‘f x = ā†‘g x) ā†’ f = g
ext
fun
_: ?m.256
_
=>
rfl: āˆ€ {Ī± : Sort ?u.258} {a : Ī±}, a = a
rfl
mul_left_inv
f: ?m.327
f
:=
ext: āˆ€ {Ī± : Type ?u.329} {Ī² : Type ?u.330} {r : Ī± ā†’ Ī± ā†’ Prop} {s : Ī² ā†’ Ī² ā†’ Prop} ā¦ƒf g : r ā‰ƒr sā¦„, (āˆ€ (x : Ī±), ā†‘f x = ā†‘g x) ā†’ f = g
ext
f: ?m.327
f
.
symm_apply_apply: āˆ€ {Ī± : Type ?u.349} {Ī² : Type ?u.350} {r : Ī± ā†’ Ī± ā†’ Prop} {s : Ī² ā†’ Ī² ā†’ Prop} (e : r ā‰ƒr s) (x : Ī±), ā†‘(RelIso.symm e) (ā†‘e x) = x
symm_apply_apply
@[simp] theorem
coe_one: ā†‘1 = id
coe_one
: ((
1: ?m.1714
1
:
r: Ī± ā†’ Ī± ā†’ Prop
r
ā‰ƒr
r: Ī± ā†’ Ī± ā†’ Prop
r
) :
Ī±: Type ?u.1683
Ī±
ā†’
Ī±: Type ?u.1683
Ī±
) =
id: {Ī± : Sort ?u.1821} ā†’ Ī± ā†’ Ī±
id
:=
rfl: āˆ€ {Ī± : Sort ?u.1862} {a : Ī±}, a = a
rfl
#align rel_iso.coe_one
RelIso.coe_one: āˆ€ {Ī± : Type u_1} {r : Ī± ā†’ Ī± ā†’ Prop}, ā†‘1 = id
RelIso.coe_one
@[simp] theorem
coe_mul: āˆ€ (eā‚ eā‚‚ : r ā‰ƒr r), ā†‘(eā‚ * eā‚‚) = ā†‘eā‚ āˆ˜ ā†‘eā‚‚
coe_mul
(
eā‚: r ā‰ƒr r
eā‚
eā‚‚: r ā‰ƒr r
eā‚‚
:
r: Ī± ā†’ Ī± ā†’ Prop
r
ā‰ƒr
r: Ī± ā†’ Ī± ā†’ Prop
r
) : ((
eā‚: r ā‰ƒr r
eā‚
*
eā‚‚: r ā‰ƒr r
eā‚‚
) :
Ī±: Type ?u.1901
Ī±
ā†’
Ī±: Type ?u.1901
Ī±
) =
eā‚: r ā‰ƒr r
eā‚
āˆ˜
eā‚‚: r ā‰ƒr r
eā‚‚
:=
rfl: āˆ€ {Ī± : Sort ?u.2880} {a : Ī±}, a = a
rfl
#align rel_iso.coe_mul
RelIso.coe_mul: āˆ€ {Ī± : Type u_1} {r : Ī± ā†’ Ī± ā†’ Prop} (eā‚ eā‚‚ : r ā‰ƒr r), ā†‘(eā‚ * eā‚‚) = ā†‘eā‚ āˆ˜ ā†‘eā‚‚
RelIso.coe_mul
theorem
mul_apply: āˆ€ {Ī± : Type u_1} {r : Ī± ā†’ Ī± ā†’ Prop} (eā‚ eā‚‚ : r ā‰ƒr r) (x : Ī±), ā†‘(eā‚ * eā‚‚) x = ā†‘eā‚ (ā†‘eā‚‚ x)
mul_apply
(
eā‚: r ā‰ƒr r
eā‚
eā‚‚: r ā‰ƒr r
eā‚‚
:
r: Ī± ā†’ Ī± ā†’ Prop
r
ā‰ƒr
r: Ī± ā†’ Ī± ā†’ Prop
r
) (
x: Ī±
x
:
Ī±: Type ?u.2929
Ī±
) : (
eā‚: r ā‰ƒr r
eā‚
*
eā‚‚: r ā‰ƒr r
eā‚‚
)
x: Ī±
x
=
eā‚: r ā‰ƒr r
eā‚
(
eā‚‚: r ā‰ƒr r
eā‚‚
x: Ī±
x
) :=
rfl: āˆ€ {Ī± : Sort ?u.3188} {a : Ī±}, a = a
rfl
#align rel_iso.mul_apply
RelIso.mul_apply: āˆ€ {Ī± : Type u_1} {r : Ī± ā†’ Ī± ā†’ Prop} (eā‚ eā‚‚ : r ā‰ƒr r) (x : Ī±), ā†‘(eā‚ * eā‚‚) x = ā†‘eā‚ (ā†‘eā‚‚ x)
RelIso.mul_apply
@[simp] theorem
inv_apply_self: āˆ€ {Ī± : Type u_1} {r : Ī± ā†’ Ī± ā†’ Prop} (e : r ā‰ƒr r) (x : Ī±), ā†‘eā»Ā¹ (ā†‘e x) = x
inv_apply_self
(
e: r ā‰ƒr r
e
:
r: Ī± ā†’ Ī± ā†’ Prop
r
ā‰ƒr
r: Ī± ā†’ Ī± ā†’ Prop
r
) (
x: Ī±
x
) :
e: r ā‰ƒr r
e
ā»Ā¹ (
e: r ā‰ƒr r
e
x: ?m.3231
x
) =
x: ?m.3231
x
:=
e: r ā‰ƒr r
e
.
symm_apply_apply: āˆ€ {Ī± : Type ?u.3356} {Ī² : Type ?u.3357} {r : Ī± ā†’ Ī± ā†’ Prop} {s : Ī² ā†’ Ī² ā†’ Prop} (e : r ā‰ƒr s) (x : Ī±), ā†‘(RelIso.symm e) (ā†‘e x) = x
symm_apply_apply
x: Ī±
x
#align rel_iso.inv_apply_self
RelIso.inv_apply_self: āˆ€ {Ī± : Type u_1} {r : Ī± ā†’ Ī± ā†’ Prop} (e : r ā‰ƒr r) (x : Ī±), ā†‘eā»Ā¹ (ā†‘e x) = x
RelIso.inv_apply_self
@[simp] theorem
apply_inv_self: āˆ€ {Ī± : Type u_1} {r : Ī± ā†’ Ī± ā†’ Prop} (e : r ā‰ƒr r) (x : Ī±), ā†‘e (ā†‘eā»Ā¹ x) = x
apply_inv_self
(
e: r ā‰ƒr r
e
:
r: Ī± ā†’ Ī± ā†’ Prop
r
ā‰ƒr
r: Ī± ā†’ Ī± ā†’ Prop
r
) (
x: Ī±
x
) :
e: r ā‰ƒr r
e
(
e: r ā‰ƒr r
e
ā»Ā¹
x: ?m.3444
x
) =
x: ?m.3444
x
:=
e: r ā‰ƒr r
e
.
apply_symm_apply: āˆ€ {Ī± : Type ?u.3569} {Ī² : Type ?u.3570} {r : Ī± ā†’ Ī± ā†’ Prop} {s : Ī² ā†’ Ī² ā†’ Prop} (e : r ā‰ƒr s) (x : Ī²), ā†‘e (ā†‘(RelIso.symm e) x) = x
apply_symm_apply
x: Ī±
x
#align rel_iso.apply_inv_self
RelIso.apply_inv_self: āˆ€ {Ī± : Type u_1} {r : Ī± ā†’ Ī± ā†’ Prop} (e : r ā‰ƒr r) (x : Ī±), ā†‘e (ā†‘eā»Ā¹ x) = x
RelIso.apply_inv_self
end RelIso