Indeks

A

abel abstraksi lambda absurd

apply, [1] argumen implisit assumption

B

bilangan real

by_cases by_contra

C

calc cases change check

congr constructor contradiction contrapose convert

D

decide

dsimp

E

eksponensial ekstensionalitas erw

exact, [1], [2] exfalso ext

F

field_simp filter fpb

from fungsi injektif fungsi monoton fungsi surjektif

G

gcd gelanggang (struktur aljabar) gelanggang komutatif

group (algebraic structure) (tactic) (taktik) grup (struktur aljabar)

H

have, [1]

hukum tiada jalan tengah

I

integrasi, [1]

intro

K

kalkulus diferensial kalkulus elementer keadaan bukti kekontinuan kesamaan definisional

keterbagian kisi konstruktor anonim konteks lokal kpk kuantor terbatas

L

lcm left let

linarith linear map logaritma

M

matrices max

min monoid

N

nilai mutlak

norm_num

O

open	operasi himpunan

P

perintah check open

pertidaksamaan push_neg

R

rcases refleksivitas relasi tatanan repeat rfl right ring (algebraic structure) (taktik)

rintro ruang bernorma ruang metrik, [1] ruang nama ruang topologi rw, [1] rwa

S

sasaran

show simp, [1]

T

tactics abel group taktik abel apply, [1] assumption by_cases by_contra dan by_contradiction calc cases change congr constructor continuity contradiction contrapose convert decide dsimp erw exact, [1], [2] exfalso ext field_simp from group have, [1] intro left let linarith noncomm_ring norm_num push_neg rcases repeat rfl dan refleksivitas right ring rintro rw dan tulis ulang, [1] rwa show simp, [1] trans use

tatanan parsial teori ukuran this topologi trans tulis ulang

U

use

V

vector space

vector subspace