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
Cmd instead 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.basic
! leanprover-community/mathlib commit f29120f82f6e24a6f6579896dfa2de6769fec962
! Please do not edit these lines, except to modify the commit id
! if you have ported upstream changes.
-/
import Mathlib.Data.FunLike.Basic
import Mathlib.Logic.Embedding.Basic
import Mathlib.Order.RelClasses
/-!
# Relation homomorphisms, embeddings, isomorphisms
This file defines relation homomorphisms, embeddings, isomorphisms and order embeddings and
isomorphisms.
## Main declarations
* `RelHom`: Relation homomorphism. A `RelHom r s` is a function `f : α → β` such that
`r a b → s (f a) (f b)`.
* `RelEmbedding`: Relation embedding. A `RelEmbedding r s` is an embedding `f : α ↪ β` such that
`r a b ↔ s (f a) (f b)`.
* `RelIso`: Relation isomorphism. A `RelIso r s` is an equivalence `f : α ≃ β` such that
`r a b ↔ s (f a) (f b)`.
* `sumLexCongr`, `prodLexCongr`: Creates a relation homomorphism between two `Sum.Lex` or two
`Prod.Lex` from relation homomorphisms between their arguments.
## Notation
* `→r`: `RelHom`
* `↪r`: `RelEmbedding`
* `≃r`: `RelIso`
-/
open Function
universe u v w
variable { α β γ δ : Type _ : Type (?u.26798+1)} { r : α → α → Prop } { s : β → β → Prop }
{ t : γ → γ → Prop } { u : δ → δ → Prop }
/-- A relation homomorphism with respect to a given pair of relations `r` and `s`
is a function `f : α → β` such that `r a b → s (f a) (f b)`. -/
structure RelHom { α β : Type _ } ( r : α → α → Prop ) ( s : β → β → Prop ) where
/-- The underlying function of a `RelHom` -/
toFun : α → β
/-- A `RelHom` sends related elements to related elements -/
map_rel' : ∀ { a b }, r a b → s ( toFun a ) ( toFun b )
#align rel_hom RelHom
/-- A relation homomorphism with respect to a given pair of relations `r` and `s`
is a function `f : α → β` such that `r a b → s (f a) (f b)`. -/
infixl :25 " →r " => RelHom
section
/-- `RelHomClass F r s` asserts that `F` is a type of functions such that all `f : F`
satisfy `r a b → s (f a) (f b)`.
The relations `r` and `s` are `outParam`s since figuring them out from a goal is a higher-order
matching problem that Lean usually can't do unaided.
-/
class RelHomClass ( F : Type _ ) { α β : outParam <| Type _ } ( r : outParam <| α → α → Prop )
( s : outParam <| β → β → Prop ) extends FunLike F α fun _ => β where
/-- A `RelHomClass` sends related elements to related elements -/
map_rel : ∀ ( f : F ) { a b }, r a b → s ( f a ) ( f b )
#align rel_hom_class RelHomClass
export RelHomClass (map_rel)
end
namespace RelHomClass
variable { F : Type _ }
protected theorem isIrrefl [ RelHomClass F r s ] ( f : F ) : ∀ [ IsIrrefl β s ], IsIrrefl α r
| ⟨ H ⟩ => ⟨ fun _ h => H _ ( map_rel f h )⟩
#align rel_hom_class.is_irrefl RelHomClass.isIrrefl
protected theorem isAsymm [ RelHomClass F r s ] ( f : F ) : ∀ [ IsAsymm β s ], IsAsymm α r
| ⟨ H : ∀ (a b : β ), s a b ¬ s b a H ⟩ => ⟨ fun _ _ h₁ h₂ => H : ∀ (a b : β ), s a b ¬ s b a H _ _ ( map_rel f h₁ ) ( map_rel f h₂ )⟩
#align rel_hom_class.is_asymm RelHomClass.isAsymm
protected theorem acc [ RelHomClass F r s ] ( f : F ) ( a : α ) : Acc s ( f a ) → Acc r a := by
generalize h : f a = b
intro ac
induction' ac with _ H : ∀ (y : ?m.9970 ), ?m.9971 y x✝ Acc ?m.9971 y H IH : ∀ (y : ?m.9970 ) (a : ?m.9971 y x✝ ?m.9972 y (_ : Acc ?m.9971 y IH generalizing a
subst h
exact ⟨ _ , fun a' h => IH : ∀ (y : β ), s y (↑f a )∀ (a : α ), ↑f a = y Acc r a IH ( f a' ) ( map_rel f h ) _ rfl : ∀ {α : Sort ?u.10178} {a : α }, a = a ⟩
#align rel_hom_class.acc RelHomClass.acc
protected theorem wellFounded [ RelHomClass F r s ] ( f : F ) : ∀ _ : WellFounded s , WellFounded r
| ⟨ H ⟩ => ⟨ fun _ => RelHomClass.acc f _ ( H _ )⟩
#align rel_hom_class.well_founded RelHomClass.wellFounded
end RelHomClass
namespace RelHom
instance : RelHomClass ( r →r s ) r s where
coe o := o . toFun : {α : Type ?u.10616} → {β : Type ?u.10615} → {r : α → α → Prop {s : β → β → Prop r →r s α → β
coe_injective' f g h := by
α : Type ?u.10508β : Type ?u.10511γ : Type ?u.10514δ : Type ?u.10517r : α → α → Prop s : β → β → Prop t : γ → γ → Prop u : δ → δ → Prop f, g : r →r s h : (fun o => o .toFun ) f = (fun o => o .toFun ) g cases f α : Type ?u.10508β : Type ?u.10511γ : Type ?u.10514δ : Type ?u.10517r : α → α → Prop s : β → β → Prop t : γ → γ → Prop u : δ → δ → Prop g : r →r s toFun✝ : α → β map_rel'✝ : ∀ {a b : α }, r a b s (toFun✝ a toFun✝ b h : (fun o => o .toFun ) { toFun := toFun✝ , map_rel' := map_rel'✝ } = (fun o => o .toFun ) g mk { toFun := toFun✝ , map_rel' := map_rel'✝ } = g
α : Type ?u.10508β : Type ?u.10511γ : Type ?u.10514δ : Type ?u.10517r : α → α → Prop s : β → β → Prop t : γ → γ → Prop u : δ → δ → Prop f, g : r →r s h : (fun o => o .toFun ) f = (fun o => o .toFun ) g cases g α : Type ?u.10508β : Type ?u.10511γ : Type ?u.10514δ : Type ?u.10517r : α → α → Prop s : β → β → Prop t : γ → γ → Prop u : δ → δ → Prop toFun✝¹ : α → β map_rel'✝¹ : ∀ {a b : α }, r a b s (toFun✝¹ a toFun✝¹ b toFun✝ : α → β map_rel'✝ : ∀ {a b : α }, r a b s (toFun✝ a toFun✝ b h : (fun o => o .toFun ) { toFun := toFun✝¹ , map_rel' := map_rel'✝¹ } = (fun o => o .toFun ) { toFun := toFun✝ , map_rel' := map_rel'✝ } mk.mk { toFun := toFun✝¹ , map_rel' := map_rel'✝¹ } = { toFun := toFun✝ , map_rel' := map_rel'✝ }
α : Type ?u.10508β : Type ?u.10511γ : Type ?u.10514δ : Type ?u.10517r : α → α → Prop s : β → β → Prop t : γ → γ → Prop u : δ → δ → Prop f, g : r →r s h : (fun o => o .toFun ) f = (fun o => o .toFun ) g congr
map_rel := map_rel' : ∀ {α : Type ?u.10659} {β : Type ?u.10658} {r : α → α → Prop s : β → β → Prop self : r →r s a b : α },
r a b s (toFun self a toFun self b
initialize_simps_projections RelHom ( toFun : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop (s : β → β → Prop r →r s α → β → apply : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop (s : β → β → Prop r →r s α → β )
protected theorem map_rel : ∀ (f : r →r s a b : α }, r a b s (↑f a ) (↑f b ) map_rel ( f : r →r s ) { a b } : r a b → s ( f a ) ( f b ) :=
f . map_rel' : ∀ {α : Type ?u.11839} {β : Type ?u.11838} {r : α → α → Prop s : β → β → Prop self : r →r s a b : α },
r a b s (toFun self a toFun self b
#align rel_hom.map_rel RelHom.map_rel : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f : r →r s a b : α }, r a b s (↑f a ) (↑f b )
@[ simp ]
theorem coe_fn_toFun : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f : r →r s f .toFun= ↑f coe_fn_toFun ( f : r →r s ) : f . toFun : {α : Type ?u.11933} → {β : Type ?u.11932} → {r : α → α → Prop {s : β → β → Prop r →r s α → β = ( f : α → β ) :=
rfl : ∀ {α : Sort ?u.12102} {a : α }, a = a
#align rel_hom.coe_fn_to_fun RelHom.coe_fn_toFun : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f : r →r s f .toFun= ↑f
/-- The map `coe_fn : (r →r s) → (α → β)` is injective. -/
theorem coe_fn_injective : Injective : {α : Sort ?u.12167} → {β : Sort ?u.12166} → (α → β Prop fun ( f : r →r s ) => ( f : α → β ) :=
FunLike.coe_injective
#align rel_hom.coe_fn_injective RelHom.coe_fn_injective
@[ ext ]
theorem ext : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f g : r →r s (∀ (x : α ), ↑f x = ↑g x ) → f = g ext ⦃ f g : r →r s ⦄ ( h : ∀ (x : α ), ↑f x = ↑g x h : ∀ x , f x = g x ) : f = g :=
FunLike.ext : ∀ {F : Sort ?u.12823} {α : Sort ?u.12824} {β : α → Sort ?u.12822i : FunLike F α β f g : F ),
(∀ (x : α ), ↑f x = ↑g x ) → f = g f g h : ∀ (x : α ), ↑f x = ↑g x h
#align rel_hom.ext RelHom.ext : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f g : r →r s (∀ (x : α ), ↑f x = ↑g x ) → f = g
theorem ext_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f g : r →r s f = g ↔ ∀ (x : α ), ↑f x = ↑g x ext_iff { f g : r →r s } : f = g ↔ ∀ x , f x = g x :=
FunLike.ext_iff : ∀ {F : Sort ?u.13310} {α : Sort ?u.13312} {β : α → Sort ?u.13311i : FunLike F α β f g : F },
f = g ↔ ∀ (x : α ), ↑f x = ↑g x
#align rel_hom.ext_iff RelHom.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f g : r →r s f = g ↔ ∀ (x : α ), ↑f x = ↑g x
/-- Identity map is a relation homomorphism. -/
@[refl, simps ]
protected def id ( r : α → α → Prop ) : r →r r :=
⟨ fun x => x , fun x => x ⟩
#align rel_hom.id RelHom.id : {α : Type u_1} → (r : α → α → Prop r →r r
#align rel_hom.id_apply RelHom.id_apply
/-- Composition of two relation homomorphisms is a relation homomorphism. -/
@[ simps ]
protected def comp : s →r t r →r s r →r t comp ( g : s →r t ) ( f : r →r s ) : r →r t :=
⟨ fun x => g ( f x ), fun h => g . 2 : ∀ {α : Type ?u.14082} {β : Type ?u.14081} {r : α → α → Prop s : β → β → Prop self : r →r s a b : α },
r a b s (toFun self a toFun self b ( f . 2 : ∀ {α : Type ?u.14116} {β : Type ?u.14115} {r : α → α → Prop s : β → β → Prop self : r →r s a b : α },
r a b s (toFun self a toFun self b h )⟩
#align rel_hom.comp RelHom.comp : {α : Type u_1} →
{β : Type u_2} →
{γ : Type u_3} → {r : α → α → Prop {s : β → β → Prop {t : γ → γ → Prop s →r t r →r s r →r t
#align rel_hom.comp_apply RelHom.comp_apply
/-- A relation homomorphism is also a relation homomorphism between dual relations. -/
protected def swap ( f : r →r s ) : swap : {α : Sort ?u.14528} →
{β : Sort ?u.14527} → {φ : α → β → Sort ?u.14526((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y r →r swap : {α : Sort ?u.14554} →
{β : Sort ?u.14553} → {φ : α → β → Sort ?u.14552((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y s :=
⟨ f , f . map_rel : ∀ {α : Type ?u.14747} {β : Type ?u.14748} {r : α → α → Prop s : β → β → Prop f : r →r s a b : α },
r a b s (↑f a ) (↑f b ) ⟩
#align rel_hom.swap RelHom.swap
/-- A function is a relation homomorphism from the preimage relation of `s` to `s`. -/
def preimage : (f : α → β (s : β → β → Prop f ⁻¹'o s →r s preimage ( f : α → β ) ( s : β → β → Prop ) : f ⁻¹'o s →r s :=
⟨ f , id : ∀ {α : Sort ?u.15059}, α → α ⟩
#align rel_hom.preimage RelHom.preimage : {α : Type u_1} → {β : Type u_2} → (f : α → β (s : β → β → Prop f ⁻¹'o s →r s
end RelHom
/-- An increasing function is injective -/
theorem injective_of_increasing ( r : α → α → Prop ) ( s : β → β → Prop ) [ IsTrichotomous α r ]
[ IsIrrefl β s ] ( f : α → β ) ( hf : ∀ {x y : α }, r x y s (f x f y
hf : ∀ { x y }, r x y → s ( f x ) ( f y )) : Injective : {α : Sort ?u.15230} → {β : Sort ?u.15229} → (α → β Prop f := by
intro x y hxy
rcases trichotomous_of r x y with (h | h | h) : r x y ∨ x = y ∨ r y x h h | h | h : r x y ∨ x = y ∨ r y x h h | h | h : r x y ∨ x = y ∨ r y x h (h | h | h) : r x y ∨ x = y ∨ r y x
· have := hf : ∀ {x y : α }, r x y s (f x f y
hf h
rw [ hxy ] at this
exfalso
exact irrefl_of : ∀ {α : Type ?u.15379} (r : α → α → Prop inst : IsIrrefl α r a : α ), ¬ r a a s ( f y ) this
· exact h
· have := hf : ∀ {x y : α }, r x y s (f x f y
hf h
rw [ hxy ] at this
exfalso
exact irrefl_of : ∀ {α : Type ?u.15437} (r : α → α → Prop inst : IsIrrefl α r a : α ), ¬ r a a s ( f y ) this
#align injective_of_increasing injective_of_increasing
/-- An increasing function is injective -/
theorem RelHom.injective_of_increasing [ IsTrichotomous α r ] [ IsIrrefl β s ] ( f : r →r s ) :
Injective : {α : Sort ?u.15541} → {β : Sort ?u.15540} → (α → β Prop f :=
_root_.injective_of_increasing r s f f . map_rel : ∀ {α : Type ?u.15886} {β : Type ?u.15887} {r : α → α → Prop s : β → β → Prop f : r →r s a b : α },
r a b s (↑f a ) (↑f b )
#align rel_hom.injective_of_increasing RelHom.injective_of_increasing
-- TODO: define a `RelIffClass` so we don't have to do all the `convert` trickery?
theorem Surjective.wellFounded_iff { f : α → β } ( hf : Surjective : {α : Sort ?u.15983} → {β : Sort ?u.15982} → (α → β Prop f )
( o : ∀ {a b : α }, r a b ↔ s (f a f b o : ∀ { a b }, r a b ↔ s ( f a ) ( f b )) :
WellFounded r ↔ WellFounded s :=
Iff.intro : ∀ {a b : Prop }, (a → b (b → a a ↔ b
( by
refine RelHomClass.wellFounded ( RelHom.mk : {α : Type ?u.16244} →
{β : Type ?u.16243} →
{r : α → α → Prop {s : β → β → Prop (toFun : α → β (∀ {a b : α }, r a b s (toFun a toFun b ) → r →r s ?_ ?_ : ∀ {a b : ?m.16245 }, ?m.16247 a b ?m.16248 (?refine_1 a ?refine_1 b
: s →r r ) refine_1 β → α
refine_2 ∀ {a b : β }, s a b r (?refine_1 a ?refine_1 b
· refine_1 β → α
refine_2 ∀ {a b : β }, s a b r (?refine_1 a ?refine_1 b
exact Classical.choose : {α : Sort ?u.16314} → {p : α → Prop (∃ x , p x ) → α hf . hasRightInverse
intro a b h
apply o : ∀ {a b : α }, r a b ↔ s (f a f b o . 2 : ∀ {a b : Prop }, (a ↔ b b → a
convert h
iterate 2 apply Classical.choose_spec hf . hasRightInverse )
( RelHomClass.wellFounded (⟨ f , o : ∀ {a b : α }, r a b ↔ s (f a f b o . 1 : ∀ {a b : Prop }, (a ↔ b a → b ⟩ : r →r s ))
#align surjective.well_founded_iff Surjective.wellFounded_iff
/-- A relation embedding with respect to a given pair of relations `r` and `s`
is an embedding `f : α ↪ β` such that `r a b ↔ s (f a) (f b)`. -/
structure RelEmbedding : {α : Type u_1} →
{β : Type u_2} →
{r : α → α → Prop {s : β → β → Prop (toEmbedding : α ↪ β (∀ {a b : α }, s (↑toEmbedding a ) (↑toEmbedding b )↔ r a b ) → RelEmbedding r s { α β : Type _ : Type (?u.17327+1)} ( r : α → α → Prop ) ( s : β → β → Prop ) extends α ↪ β where
/-- Elements are related iff they are related after apply a `RelEmbedding` -/
map_rel_iff' : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop self : RelEmbedding r s a b : α },
s (↑self .toEmbeddinga ) (↑self .toEmbeddingb )↔ r a b : ∀ { a b }, s ( toEmbedding a ) ( toEmbedding b ) ↔ r a b
#align rel_embedding RelEmbedding
/-- A relation embedding with respect to a given pair of relations `r` and `s`
is an embedding `f : α ↪ β` such that `r a b ↔ s (f a) (f b)`. -/
infixl :25 " ↪r " => RelEmbedding
/-- The induced relation on a subtype is an embedding under the natural inclusion. -/
def Subtype.relEmbedding : {X : Type ?u.26060} → (r : X → X → Prop (p : X → Prop val ⁻¹'o r ↪r r Subtype.relEmbedding { X : Type _ : Type (?u.26060+1)} ( r : X → X → Prop ) ( p : X → Prop ) :
( Subtype.val : Subtype : {α : Sort ?u.26087} → (α → Prop Sort (max1?u.26087) p → X ) ⁻¹'o r ↪r r :=
⟨ Embedding.subtype p , Iff.rfl : ∀ {a : Prop }, a ↔ a ⟩
#align subtype.rel_embedding Subtype.relEmbedding : {X : Type u_1} → (r : X → X → Prop (p : X → Prop Subtype.val ⁻¹'o r ↪r r
theorem preimage_equivalence { α β } ( f : α → β ) { s : β → β → Prop } ( hs : Equivalence s ) :
Equivalence ( f ⁻¹'o s ) :=
⟨ fun _ => hs . 1 _ , fun h => hs . 2 h , fun h₁ h₂ => hs . 3 : ∀ {α : Sort ?u.26446} {r : α → α → Prop Equivalence r ∀ {x y z : α }, r x y r y z r x z h₁ h₂ ⟩
#align preimage_equivalence preimage_equivalence
namespace RelEmbedding
/-- A relation embedding is also a relation homomorphism -/
def toRelHom : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop {s : β → β → Prop r ↪r s r →r s toRelHom ( f : r ↪r s ) : r →r s where
toFun := f . toEmbedding : {α : Type ?u.26577} → {β : Type ?u.26576} → {r : α → α → Prop {s : β → β → Prop r ↪r s α ↪ β . toFun : {α : Sort ?u.26595} → {β : Sort ?u.26594} → (α ↪ β α → β
map_rel' := ( map_rel_iff' : ∀ {α : Type ?u.26606} {β : Type ?u.26605} {r : α → α → Prop s : β → β → Prop self : r ↪r s a b : α },
s (↑self .toEmbeddinga ) (↑self .toEmbeddingb )↔ r a b f ). mpr : ∀ {a b : Prop }, (a ↔ b b → a mpr
#align rel_embedding.to_rel_hom RelEmbedding.toRelHom : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop {s : β → β → Prop r ↪r s r →r s
instance : Coe ( r ↪r s ) ( r →r s ) :=
⟨ toRelHom : {α : Type ?u.26876} → {β : Type ?u.26875} → {r : α → α → Prop {s : β → β → Prop r ↪r s r →r s ⟩
--Porting note: removed
-- see Note [function coercion]
-- instance : CoeFun (r ↪r s) fun _ => α → β :=
-- ⟨fun o => o.toEmbedding⟩
-- TODO: define and instantiate a `RelEmbeddingClass` when `EmbeddingLike` is defined
instance : RelHomClass ( r ↪r s ) r s where
coe := fun x => x . toFun : {α : Sort ?u.27196} → {β : Sort ?u.27195} → (α ↪ β α → β
coe_injective' f g h := by
α : Type ?u.27070β : Type ?u.27073γ : Type ?u.27076δ : Type ?u.27079r : α → α → Prop s : β → β → Prop t : γ → γ → Prop u : δ → δ → Prop f, g : r ↪r s h : (fun x => x .toFun ) f = (fun x => x .toFun ) g rcases f with ⟨ ⟨⟩ ⟩ α : Type ?u.27070β : Type ?u.27073γ : Type ?u.27076δ : Type ?u.27079r : α → α → Prop s : β → β → Prop t : γ → γ → Prop u : δ → δ → Prop g : r ↪r s toFun✝ : α → β inj'✝ : Injective toFun✝ map_rel_iff'✝ : ∀ {a b : α }, s (↑{ toFun := toFun✝ , inj' := inj'✝ } a ) (↑{ toFun := toFun✝ , inj' := inj'✝ } b )↔ r a b h : (fun x => x .toFun ) { toEmbedding := { toFun := toFun✝ , inj' := inj'✝ } , map_rel_iff' := map_rel_iff'✝ } = (fun x => x .toFun ) g mk.mk { toEmbedding := { toFun := toFun✝ , inj' := inj'✝ } , map_rel_iff' := map_rel_iff'✝ } = g
α : Type ?u.27070β : Type ?u.27073γ : Type ?u.27076δ : Type ?u.27079r : α → α → Prop s : β → β → Prop t : γ → γ → Prop u : δ → δ → Prop f, g : r ↪r s h : (fun x => x .toFun ) f = (fun x => x .toFun ) g rcases g with ⟨ ⟨⟩ ⟩ α : Type ?u.27070β : Type ?u.27073γ : Type ?u.27076δ : Type ?u.27079r : α → α → Prop s : β → β → Prop t : γ → γ → Prop u : δ → δ → Prop toFun✝¹ : α → β inj'✝¹ : Injective toFun✝¹ map_rel_iff'✝¹ : ∀ {a b : α }, s (↑{ toFun := toFun✝¹ , inj' := inj'✝¹ } a ) (↑{ toFun := toFun✝¹ , inj' := inj'✝¹ } b )↔ r a b toFun✝ : α → β inj'✝ : Injective toFun✝ map_rel_iff'✝ : ∀ {a b : α }, s (↑{ toFun := toFun✝ , inj' := inj'✝ } a ) (↑{ toFun := toFun✝ , inj' := inj'✝ } b )↔ r a b h : (fun x => x .toFun ) { toEmbedding := { toFun := toFun✝¹ , inj' := inj'✝¹ } , map_rel_iff' := map_rel_iff'✝¹ } = (fun x => x .toFun ) { toEmbedding := { toFun := toFun✝ , inj' := inj'✝ } , map_rel_iff' := map_rel_iff'✝ } mk.mk.mk.mk { toEmbedding := { toFun := toFun✝¹ , inj' := inj'✝¹ } , map_rel_iff' := map_rel_iff'✝¹ } = { toEmbedding := { toFun := toFun✝ , inj' := inj'✝ } , map_rel_iff' := map_rel_iff'✝ }
α : Type ?u.27070β : Type ?u.27073γ : Type ?u.27076δ : Type ?u.27079r : α → α → Prop s : β → β → Prop t : γ → γ → Prop u : δ → δ → Prop f, g : r ↪r s h : (fun x => x .toFun ) f = (fun x => x .toFun ) g congr
map_rel f a b := Iff.mpr : ∀ {a b : Prop }, (a ↔ b b → a ( map_rel_iff' : ∀ {α : Type ?u.27240} {β : Type ?u.27239} {r : α → α → Prop s : β → β → Prop self : r ↪r s a b : α },
s (↑self .toEmbeddinga ) (↑self .toEmbeddingb )↔ r a b f )
/-- See Note [custom simps projection]. We specify this explicitly because we have a coercion not
given by the `FunLike` instance. Todo: remove that instance?
-/
def Simps.apply : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop {s : β → β → Prop r ↪r s α → β Simps.apply ( h : r ↪r s ) : α → β :=
h
initialize_simps_projections RelEmbedding ( toFun : {α : Type u_1} → {β : Type u_2} → (r : α → α → Prop (s : β → β → Prop r ↪r s α → β → apply : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop {s : β → β → Prop r ↪r s α → β )
@[ simp ]
theorem coe_toEmbedding : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f : r ↪r s ↑f .toEmbedding = ↑f coe_toEmbedding : ( ( f : r ↪r s ) . toEmbedding : {α : Type ?u.28693} → {β : Type ?u.28692} → {r : α → α → Prop {s : β → β → Prop r ↪r s α ↪ β toEmbedding : α → β ) = f :=
rfl : ∀ {α : Sort ?u.29211} {a : α }, a = a
#align rel_embedding.coe_fn_to_embedding RelEmbedding.coe_toEmbedding : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f : r ↪r s ↑f .toEmbedding = ↑f
@[ simp ]
theorem coe_toRelHom : ( ( f : r ↪r s ) . toRelHom : {α : Type ?u.29342} → {β : Type ?u.29341} → {r : α → α → Prop {s : β → β → Prop r ↪r s r →r s toRelHom : α → β ) = f :=
rfl : ∀ {α : Sort ?u.29882} {a : α }, a = a
theorem injective ( f : r ↪r s ) : Injective : {α : Sort ?u.29992} → {β : Sort ?u.29991} → (α → β Prop f :=
f . inj'
#align rel_embedding.injective RelEmbedding.injective
theorem inj : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α }, ↑f a = ↑f b ↔ a = b inj ( f : r ↪r s ) { a b } : f a = f b ↔ a = b :=
f . injective . eq_iff : ∀ {α : Sort ?u.30519} {β : Sort ?u.30520} {f : α → β Injective f ∀ {a b : α }, f a = f b ↔ a = b
#align rel_embedding.inj RelEmbedding.inj : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α }, ↑f a = ↑f b ↔ a = b
theorem map_rel_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α }, s (↑f a ) (↑f b )↔ r a b map_rel_iff ( f : r ↪r s ) { a b } : s ( f a ) ( f b ) ↔ r a b :=
f . map_rel_iff' : ∀ {α : Type ?u.30879} {β : Type ?u.30878} {r : α → α → Prop s : β → β → Prop self : r ↪r s a b : α },
s (↑self .toEmbeddinga ) (↑self .toEmbeddingb )↔ r a b
#align rel_embedding.map_rel_iff RelEmbedding.map_rel_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α }, s (↑f a ) (↑f b )↔ r a b
@[ simp ]
theorem coe_mk : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f : α ↪ β h : ∀ {a b : α }, s (↑f a ) (↑f b )↔ r a b }, ↑{ toEmbedding := f , map_rel_iff' := h } = ↑f coe_mk : ⇑(⟨ f , h ⟩ : r ↪r s ) = f :=
rfl : ∀ {α : Sort ?u.31583} {a : α }, a = a
#align rel_embedding.coe_fn_mk RelEmbedding.coe_mk : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f : α ↪ β h : ∀ {a b : α }, s (↑f a ) (↑f b )↔ r a b }, ↑{ toEmbedding := f , map_rel_iff' := h } = ↑f
/-- The map `coe_fn : (r ↪r s) → (α → β)` is injective. -/
theorem coe_fn_injective : Injective : {α : Sort ?u.31685} → {β : Sort ?u.31684} → (α → β Prop fun f : r ↪r s => ( f : α → β ) :=
FunLike.coe_injective
#align rel_embedding.coe_fn_injective RelEmbedding.coe_fn_injective
@[ ext ]
theorem ext : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f g : r ↪r s (∀ (x : α ), ↑f x = ↑g x ) → f = g ext ⦃ f g : r ↪r s ⦄ ( h : ∀ (x : α ), ↑f x = ↑g x h : ∀ x , f x = g x ) : f = g :=
FunLike.ext : ∀ {F : Sort ?u.32341} {α : Sort ?u.32342} {β : α → Sort ?u.32340i : FunLike F α β f g : F ),
(∀ (x : α ), ↑f x = ↑g x ) → f = g _ _ h : ∀ (x : α ), ↑f x = ↑g x h
#align rel_embedding.ext RelEmbedding.ext : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f g : r ↪r s (∀ (x : α ), ↑f x = ↑g x ) → f = g
theorem ext_iff : ∀ {f g : r ↪r s f = g ↔ ∀ (x : α ), ↑f x = ↑g x ext_iff { f g : r ↪r s } : f = g ↔ ∀ x , f x = g x :=
FunLike.ext_iff : ∀ {F : Sort ?u.32842} {α : Sort ?u.32844} {β : α → Sort ?u.32843i : FunLike F α β f g : F },
f = g ↔ ∀ (x : α ), ↑f x = ↑g x
#align rel_embedding.ext_iff RelEmbedding.ext_iff : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f g : r ↪r s f = g ↔ ∀ (x : α ), ↑f x = ↑g x
/-- Identity map is a relation embedding. -/
@[refl, simps! ]
protected def refl : (r : α → α → Prop r ↪r r refl ( r : α → α → Prop ) : r ↪r r :=
⟨ Embedding.refl : (α : Sort ?u.33076) → α ↪ α _ , Iff.rfl : ∀ {a : Prop }, a ↔ a ⟩
#align rel_embedding.refl RelEmbedding.refl : {α : Type u_1} → (r : α → α → Prop r ↪r r
#align rel_embedding.refl_apply RelEmbedding.refl_apply
/-- Composition of two relation embeddings is a relation embedding. -/
protected def trans ( f : r ↪r s ) ( g : s ↪r t ) : r ↪r t :=
⟨ f . 1 : {α : Type ?u.33321} → {β : Type ?u.33320} → {r : α → α → Prop {s : β → β → Prop r ↪r s α ↪ β . trans : {α : Sort ?u.33340} → {β : Sort ?u.33339} → {γ : Sort ?u.33338} → (α ↪ β (β ↪ γ α ↪ γ trans g . 1 : {α : Type ?u.33354} → {β : Type ?u.33353} → {r : α → α → Prop {s : β → β → Prop r ↪r s α ↪ β , by simp [ f . map_rel_iff : ∀ {α : Type ?u.33376} {β : Type ?u.33377} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α },
s (↑f a ) (↑f b )↔ r a b , g . map_rel_iff : ∀ {α : Type ?u.33428} {β : Type ?u.33429} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α },
s (↑f a ) (↑f b )↔ r a b ] ⟩
#align rel_embedding.trans RelEmbedding.trans : {α : Type u_1} →
{β : Type u_2} →
{γ : Type u_3} → {r : α → α → Prop {s : β → β → Prop {t : γ → γ → Prop r ↪r s s ↪r t r ↪r t
instance ( r : α → α → Prop ) : Inhabited : Sort ?u.34927 → Sort (max1?u.34927) ( r ↪r r ) :=
⟨ RelEmbedding.refl : {α : Type ?u.34951} → (r : α → α → Prop r ↪r r _ : ?m.34952 → ?m.34952 → Prop ⟩
theorem trans_apply ( f : r ↪r s ) ( g : s ↪r t ) ( a : α ) : ( f . trans : {α : Type ?u.35133} →
{β : Type ?u.35132} →
{γ : Type ?u.35131} → {r : α → α → Prop {s : β → β → Prop {t : γ → γ → Prop r ↪r s s ↪r t r ↪r t g ) a = g ( f a ) :=
rfl : ∀ {α : Sort ?u.35609} {a : α }, a = a
#align rel_embedding.trans_apply RelEmbedding.trans_apply
@[ simp ]
theorem coe_trans ( f : r ↪r s ) ( g : s ↪r t ) : ( f . trans : {α : Type ?u.35710} →
{β : Type ?u.35709} →
{γ : Type ?u.35708} → {r : α → α → Prop {s : β → β → Prop {t : γ → γ → Prop r ↪r s s ↪r t r ↪r t g ) = g ∘ f :=
rfl : ∀ {α : Sort ?u.36637} {a : α }, a = a
#align rel_embedding.coe_trans RelEmbedding.coe_trans
/-- A relation embedding is also a relation embedding between dual relations. -/
protected def swap ( f : r ↪r s ) : swap : {α : Sort ?u.36772} →
{β : Sort ?u.36771} → {φ : α → β → Sort ?u.36770((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y r ↪r swap : {α : Sort ?u.36798} →
{β : Sort ?u.36797} → {φ : α → β → Sort ?u.36796((x : α ) → (y : β ) → φ x y ) → (y : β ) → (x : α ) → φ x y s :=
⟨ f . toEmbedding : {α : Type ?u.36849} → {β : Type ?u.36848} → {r : α → α → Prop {s : β → β → Prop r ↪r s α ↪ β , f . map_rel_iff : ∀ {α : Type ?u.36862} {β : Type ?u.36863} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α },
s (↑f a ) (↑f b )↔ r a b ⟩
#align rel_embedding.swap RelEmbedding.swap
/-- If `f` is injective, then it is a relation embedding from the
preimage relation of `s` to `s`. -/
def preimage ( f : α ↪ β ) ( s : β → β → Prop ) : f ⁻¹'o s ↪r s :=
⟨ f , Iff.rfl : ∀ {a : Prop }, a ↔ a ⟩
#align rel_embedding.preimage RelEmbedding.preimage : {α : Type u_1} → {β : Type u_2} → (f : α ↪ β (s : β → β → Prop ↑f ⁻¹'o s ↪r s
theorem eq_preimage ( f : r ↪r s ) : r = f ⁻¹'o s := by
ext ( a b )
exact f . map_rel_iff : ∀ {α : Type ?u.37687} {β : Type ?u.37688} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α },
s (↑f a ) (↑f b )↔ r a b . symm : ∀ {a b : Prop }, (a ↔ b b ↔ a
#align rel_embedding.eq_preimage RelEmbedding.eq_preimage : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop s : β → β → Prop f : r ↪r s r = ↑f ⁻¹'o s
protected theorem isIrrefl ( f : r ↪r s ) [ IsIrrefl β s ] : IsIrrefl α r :=
⟨ fun a => mt : ∀ {a b : Prop }, (a → b ¬ b ¬ a f . map_rel_iff : ∀ {α : Type ?u.37818} {β : Type ?u.37819} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α },
s (↑f a ) (↑f b )↔ r a b . 2 : ∀ {a b : Prop }, (a ↔ b b → a ( irrefl : ∀ {α : Type ?u.37847} {r : α → α → Prop inst : IsIrrefl α r a : α ), ¬ r a a ( f a ))⟩
#align rel_embedding.is_irrefl RelEmbedding.isIrrefl
protected theorem isRefl ( f : r ↪r s ) [ IsRefl β s ] : IsRefl α r :=
⟨ fun _ => f . map_rel_iff : ∀ {α : Type ?u.38114} {β : Type ?u.38115} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α },
s (↑f a ) (↑f b )↔ r a b . 1 : ∀ {a b : Prop }, (a ↔ b a → b <| refl : ∀ {α : Type ?u.38140} {r : α → α → Prop inst : IsRefl α r a : α ), r a a _ ⟩
#align rel_embedding.is_refl RelEmbedding.isRefl
protected theorem isSymm ( f : r ↪r s ) [ IsSymm β s ] : IsSymm α r :=
⟨ fun _ _ => imp_imp_imp : ∀ {a b c d : Prop }, (c → a (b → d (a → b c → d f . map_rel_iff : ∀ {α : Type ?u.38282} {β : Type ?u.38283} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α },
s (↑f a ) (↑f b )↔ r a b . 2 : ∀ {a b : Prop }, (a ↔ b b → a f . map_rel_iff : ∀ {α : Type ?u.38311} {β : Type ?u.38312} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α },
s (↑f a ) (↑f b )↔ r a b . 1 : ∀ {a b : Prop }, (a ↔ b a → b symm : ∀ {α : Type ?u.38328} {r : α → α → Prop inst : IsSymm α r a b : α }, r a b r b a ⟩
#align rel_embedding.is_symm RelEmbedding.isSymm
protected theorem isAsymm ( f : r ↪r s ) [ IsAsymm β s ] : IsAsymm α r :=
⟨ fun _ _ h₁ h₂ => asymm : ∀ {α : Type ?u.38471} {r : α → α → Prop inst : IsAsymm α r a b : α }, r a b ¬ r b a ( f . map_rel_iff : ∀ {α : Type ?u.38477} {β : Type ?u.38478} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α },
s (↑f a ) (↑f b )↔ r a b . 2 : ∀ {a b : Prop }, (a ↔ b b → a h₁ ) ( f . map_rel_iff : ∀ {α : Type ?u.38518} {β : Type ?u.38519} {r : α → α → Prop s : β → β → Prop f : r ↪r s a b : α },
s (↑f a ) (↑f b )↔ r a b . 2 : ∀ {a b : Prop }, (a ↔ b b → a h₂ )⟩
#align rel_embedding.is_asymm RelEmbedding.isAsymm
protected theorem isAntisymm : ∀ ( _ : r ↪r s ) [ IsAntisymm β s ], IsAntisymm α r
| ⟨ f , o : ∀ {a b : α }, s (↑f a ) (↑f b )↔ r a b o ⟩, ⟨ H : ∀ (a b : β ), s a b s b a a = b H ⟩ => ⟨ fun _ _ h₁ h₂ => f . inj' ( H : ∀ (a b : β ), s a b s b a a = b H _ _ ( o : ∀ {a b : α }, s (↑f a ) (↑f b )↔ r a b o . 2 : ∀ {a b : Prop }, (a ↔ b b → a h₁ ) ( o : ∀ {a b : α }, s (↑f a ) (↑f b )↔ r a b o . 2 : ∀ {a b : Prop }, (a ↔ b b → a h₂ ))⟩
#align rel_embedding.is_antisymm RelEmbedding.isAntisymm
protected theorem isTrans : ∀ ( _ : r ↪r s ) [ IsTrans β s ], IsTrans α r
| ⟨_, o : ∀ {a b : α }, s (↑toEmbedding✝ a ) (↑toEmbedding✝ b )↔ r a b o ⟩, ⟨ H : ∀ (a b c : β ), s a b s b c s a c
H ⟩ => ⟨ fun _ _ _ h₁ h₂ => o : ∀ {a b : α }, s (↑toEmbedding✝ a ) (↑toEmbedding✝ b )↔ r a b o . 1 : ∀ {a b : Prop }, (a ↔ b a → b ( H : ∀ (a b c : β ), s a b s b c s a c
H _ _ _ ( o : ∀ {a b : α }, s (↑toEmbedding✝ a ) (↑toEmbedding✝ b )↔ r a b o . 2 : ∀ {a b : Prop }, (a ↔ b b → a h₁ ) ( o : ∀ {a b : α }, s (↑toEmbedding✝ a ) (↑toEmbedding✝ b )↔ r a b o . 2 : ∀ {a b : Prop }, (a ↔ b b → a h₂ ))⟩
#align rel_embedding.is_trans RelEmbedding.isTrans
protected theorem isTotal : ∀ ( _ : r ↪r s ) [ IsTotal β s ], IsTotal α r
| ⟨_, o : ∀ {a b : α }, s (↑toEmbedding✝ a ) (↑toEmbedding✝ b )↔ r a b o ⟩, ⟨ H : ∀ (a b : β ), s a b ∨ s b a H ⟩ => ⟨ fun _ _ => ( or_congr : ∀ {a c b d : Prop }, (a ↔ c (b ↔ d a ∨ b ↔ c ∨ d o : ∀ {a b : α }, s (↑toEmbedding✝ a ) (↑toEmbedding✝ b )↔ r a b o o : ∀ {a b : α }, s (↑toEmbedding✝ a ) (↑toEmbedding✝ b )↔ r a b o ). 1 : ∀ {a b : Prop }, (a ↔ b a → b ( H : ∀ (a b : β ), s a b ∨ s b a H _ _ )⟩
#align rel_embedding.is_total RelEmbedding.isTotal
protected theorem isPreorder : ∀ ( _ : r ↪r s ) [ IsPreorder β s ], IsPreorder α r
| f , _ => { f.isRefl, f.isTrans with } : IsPreorder ?m.40049 ?m.40050 f { f.isRefl, f.isTrans with } : IsPreorder ?m.40049 ?m.40050 isRefl { f.isRefl, f.isTrans with } : IsPreorder ?m.40049 ?m.40050 f { f.isRefl, f.isTrans with } : IsPreorder ?m.40049 ?m.40050 isTrans { f.isRefl, f.isTrans with } : IsPreorder ?m.40049 ?m.40050 { f.isRefl, f.isTrans with } : IsPreorder ?m.40049 ?m.40050 with { f.isRefl, f.isTrans with } : IsPreorder ?m.40049 ?m.40050
#align rel_embedding.is_preorder RelEmbedding.isPreorder
protected theorem isPartialOrder : ∀ ( _ : r ↪r s ) [ IsPartialOrder β s ], IsPartialOrder α r
| f , _ => { f . isPreorder , f . isAntisymm with }
#align rel_embedding.is_partial_order RelEmbedding.isPartialOrder
protected theorem isLinearOrder : ∀ ( _ : r ↪r s ) [ IsLinearOrder β s ], IsLinearOrder α r
| f , _ => { f.isPartialOrder, f.isTotal wit