Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - lint(src/order/rel_iso): docstrings and inhabited #4441

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - lint(src/order/rel_iso): docstrings and inhabited #4441

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 15 additions & 2 deletions src/order/rel_iso.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -173,6 +173,8 @@ theorem ext_iff {f g : r ↪r s} : f = g ↔ ∀ x, f x = g x :=
@[trans] protected def trans (f : r ↪r s) (g : s ↪r t) : r ↪r t :=
⟨f.1.trans g.1, λ a b, by rw [f.2, g.2]; simp⟩

instance (r : α → α → Prop) : inhabited (r ↪r r) := ⟨rel_embedding.refl _⟩

@[simp] theorem refl_apply (x : α) : rel_embedding.refl r x = x := rfl

@[simp] theorem trans_apply (f : r ↪r s) (g : s ↪r t) (a : α) : (f.trans g) a = g (f a) := rfl
Expand Down Expand Up @@ -379,6 +381,8 @@ theorem ext_iff {f g : r ≃r s} : f = g ↔ ∀ x, f x = g x :=
@[trans] protected def trans (f₁ : r ≃r s) (f₂ : s ≃r t) : r ≃r t :=
⟨f₁.to_equiv.trans f₂.to_equiv, λ a b, f₁.map_rel_iff.trans f₂.map_rel_iff⟩

instance (r : α → α → Prop) : inhabited (r ≃r r) := ⟨rel_iso.refl _⟩

/-- a relation isomorphism is also a relation isomorphism between dual relations. -/
protected def swap (f : r ≃r s) : (swap r) ≃r (swap s) :=
⟨f.to_equiv, λ _ _, f.map_rel_iff⟩
Expand Down Expand Up @@ -417,13 +421,21 @@ noncomputable def of_surjective (f : r ↪r s) (H : surjective f) : r ≃r s :=
@[simp] theorem of_surjective_coe (f : r ↪r s) (H) : (of_surjective f H : α → β) = f :=
rfl

/--
Given relation isomorphisms `r₁ ≃r r₂` and `s₁ ≃r s₂`, construct a relation isomorphism for the
lexicographic orders on the sum.
-/
def sum_lex_congr {α₁ α₂ β₁ β₂ r₁ r₂ s₁ s₂}
(e₁ : @rel_iso α₁ α₂ r₁ r₂) (e₂ : @rel_iso β₁ β₂ s₁ s₂) :
sum.lex r₁ s₁ ≃r sum.lex r₂ s₂ :=
⟨equiv.sum_congr e₁.to_equiv e₂.to_equiv, λ a b,
by cases e₁ with f hf; cases e₂ with g hg;
cases a; cases b; simp [hf, hg]⟩

/--
Given relation isomorphisms `r₁ ≃r r₂` and `s₁ ≃r s₂`, construct a relation isomorphism for the
lexicographic orders on the product.
-/
def prod_lex_congr {α₁ α₂ β₁ β₂ r₁ r₂ s₁ s₂}
(e₁ : @rel_iso α₁ α₂ r₁ r₂) (e₂ : @rel_iso β₁ β₂ s₁ s₂) :
prod.lex r₁ s₁ ≃r prod.lex r₂ s₂ :=
Expand Down Expand Up @@ -466,7 +478,7 @@ end rel_iso

namespace order_iso

/-- Reinterpret an order isomorphism as an order embedding-/
/-- Reinterpret an order isomorphism as an order embedding. -/
def to_order_embedding [has_le α] [has_le β] (e : α ≃o β) : α ↪o β :=
e.to_rel_embedding

Expand All @@ -493,6 +505,7 @@ def subrel (r : α → α → Prop) (p : set α) : p → p → Prop :=

namespace subrel

/-- The relation embedding from the inherited relation on a subset. -/
protected def rel_embedding (r : α → α → Prop) (p : set α) :
subrel r p ↪r r := ⟨set_coe_embedding _, λ a b, iff.rfl⟩

Expand All @@ -505,7 +518,7 @@ rel_embedding.is_well_order (subrel.rel_embedding r p)

end subrel

/-- Restrict the codomain of a relation embedding -/
/-- Restrict the codomain of a relation embedding. -/
def rel_embedding.cod_restrict (p : set β) (f : r ↪r s) (H : ∀ a, f a ∈ p) : r ↪r subrel s p :=
⟨f.to_embedding.cod_restrict p H, f.map_rel_iff'⟩

Expand Down