Theorems · Theorem · logic and foundations

RelEmbedding.ofMonotone.congr_simp

∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} [inst : Std.Trichotomous r] [inst_1 : Std.Asymm s]
  (f f_1 : α → β) (e_f : f = f_1) (H : ∀ (a b : α), r a b → s (f a) (f b)),
  RelEmbedding.ofMonotone f H = RelEmbedding.ofMonotone f_1 ⋯

Defined in: Mathlib.SetTheory.Ordinal.Univ
Cited by: 0 results in Mathlib
Foundations: Depth 15 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Std.Trichotomous Std.Asymm

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

RelEmbeddingstatement · cited by 281
RelEmbedding.ofMonotonestatement and proof · cited by 5

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.